style: replace ← pure with := in matches

leanprover-community · Nov 2, 2024 · b7ff016 · b7ff016
1 parent 1357f4f
commit b7ff016
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
@@ -8,7 +8,7 @@ def throwFailedToEval (e : Expr) : MetaM α :=
 
 private partial def evalList [ReduceEval α] (e : Expr) : MetaM (List α) := do
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwFailedToEval e
+  let .const c _ := e.getAppFn | throwFailedToEval e
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``List.nil, 1 => pure []

diff --git a/Qq/Macro.lean b/Qq/Macro.lean
@@ -254,7 +254,7 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do
     }
     return fv
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
+  let .const c _ := e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``betaRev', 2 => return betaRev' (← unquoteExpr (e.getArg! 0)) (← unquoteExprList (e.getArg! 1))