diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 1652e7e3c6..98c78e1cec 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -66,7 +66,7 @@ private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) Macro
else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
let term := args.get! 1;
term ← expandLiftMethodAux term;
- auxDo ← `(do a ← $term; $(Syntax.missing));
+ auxDo ← `(do let a ← $term; $(Syntax.missing));
let auxDoElems := (getDoElems auxDo).pop;
modify $ fun s => s ++ auxDoElems;
`(a)
@@ -117,7 +117,9 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
rest ← mkRest ();
newBody ← `(let $letDecl:letDecl; $rest);
addPrefix newBody
- else if doElem.getKind == `Lean.Parser.Term.doPat then withFreshMacroScope $ do
+ -- cleanup the following code
+ else if doElem.getKind == `Lean.Parser.Term.doLetArrow && (doElem.getArg 1).getKind == `Lean.Parser.Term.doPat then withFreshMacroScope $ do
+ let doElem := doElem.getArg 1;
-- (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
let pat := doElem.getArg 0;
let discr := doElem.getArg 2;
@@ -125,15 +127,15 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
rest ← mkRest ();
newBody ←
if optElse.isNone then do
- `(do x ← $discr; match x with | $pat => $rest)
+ `(do let x ← $discr; match x with | $pat => $rest)
else
let elseBody := optElse.getArg 1;
- `(do x ← $discr; match x with | $pat => $rest | _ => $elseBody);
+ `(do let x ← $discr; match x with | $pat => $rest | _ => $elseBody);
addPrefix newBody
else if i < doElems.size - 1 && doElem.getKind == `Lean.Parser.Term.doExpr then do
-- def doExpr := parser! termParser
let term := doElem.getArg 0;
- auxDo ← `(do x ← $term; $(Syntax.missing));
+ auxDo ← `(do let x ← $term; $(Syntax.missing));
let doElemNew := (getDoElems auxDo).get! 0;
let doElems := doElems.set! i doElemNew;
expandDoElems true doElems (i+2)
@@ -193,9 +195,10 @@ private partial def processDoElemsAux (doElems : Array Syntax) (m bindInstVal :
let doElem := doElems.get! i;
let k := doElem.getKind;
withRef doElem $
- if k == `Lean.Parser.Term.doId then do
+ if k == `Lean.Parser.Term.doLetArrow then do
when (i == doElems.size - 1) $
throwError "the last statement in a 'do' block must be an expression";
+ let doElem := doElem.getArg 1;
-- try (ident >> optType >> leftArrow) >> termParser
let id := doElem.getIdAt 0;
let typeStx := expandOptType doElem (doElem.getArg 1);
diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean
index 80ee6241a7..858b2acf9c 100644
--- a/tests/compiler/termparsertest1.lean
+++ b/tests/compiler/termparsertest1.lean
@@ -104,14 +104,14 @@ match x with
"¬ a ∧ b",
"
do
- x ← f a;
- x : Nat ← f a;
+ let x ← f a;
+ let x : Nat ← f a;
g x;
let y := g x;
- (a, b) <- h x y;
+ let (a, b) <- h x y;
let (a, b) := (b, a);
pure (a + b)",
-"do { x ← f a; pure $ a + a }",
+"do { let x ← f a; pure $ a + a }",
"let f : Nat → Nat → Nat
| 0, a => a + 10
| n+1, b => n * b;
diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index 70c44f74b7..ba04d37705 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -265,24 +265,24 @@ let x[i] := f 20; x
(Term.and (Term.not "¬" `a) "∧" `b)
do
- x ← f a;
- x : Nat ← f a;
+ let x ← f a;
+ let x : Nat ← f a;
g x;
let y := g x;
- (a, b) <- h x y;
+ let (a, b) <- h x y;
let (a, b) := (b, a);
pure (a + b)
(Term.do
"do"
- [(Term.doId `x [] "←" (Term.app `f [`a]))
+ [(Term.doLetArrow "let" (Term.doId `x [] "←" (Term.app `f [`a])))
";"
- (Term.doId `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a]))
+ (Term.doLetArrow "let" (Term.doId `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a])))
";"
(Term.doExpr (Term.app `g [`x]))
";"
(Term.doLet "let" (Term.letDecl (Term.letIdDecl `y [] [] ":=" (Term.app `g [`x]))))
";"
- (Term.doPat (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) [])
+ (Term.doLetArrow "let" (Term.doPat (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) []))
";"
(Term.doLet
"let"
@@ -296,12 +296,14 @@ do
";"
(Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")]))]
[])
-do { x ← f a; pure $ a + a }
+do { let x ← f a; pure $ a + a }
(Term.do
"do"
(Term.doSeqBracketed
"{"
- [(Term.doId `x [] "←" (Term.app `f [`a])) ";" (Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a)))]
+ [(Term.doLetArrow "let" (Term.doId `x [] "←" (Term.app `f [`a])))
+ ";"
+ (Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a)))]
"}"))
let f : Nat → Nat → Nat
| 0, a => a + 10
diff --git a/tests/lean/IRbug.lean b/tests/lean/IRbug.lean
index 94dff46f71..8adc37f9fe 100644
--- a/tests/lean/IRbug.lean
+++ b/tests/lean/IRbug.lean
@@ -14,10 +14,10 @@ instance : Monad FooM := {}
def unexpectedBehavior : FooM String := do
let b : Bool := (#[] : Array Nat).isEmpty;
-trueBranch ← pure "trueBranch";
-falseBranch ← pure "falseBranch";
+let trueBranch ← pure "trueBranch";
+let falseBranch ← pure "falseBranch";
(1 : Nat).foldM (λ _ (s : String) => do
- s ← pure $ if b then trueBranch else falseBranch; pure s) ""
+ let s ← pure $ if b then trueBranch else falseBranch; pure s) ""
#eval unexpectedBehavior ()
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index e0f91648a7..56d2ac2a96 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -9,18 +9,18 @@ open Lean.Format
open Lean.Meta
def check (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : TermElabM Unit := do
-opts ← getOptions;
-stx ← stx;
-e ← elabTermAndSynthesize stx none <* throwErrorIfErrors;
-stx' ← liftMetaM $ delab Name.anonymous [] e optionsPerPos;
-stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx';
-f' ← liftCoreM $ PrettyPrinter.formatTerm stx';
+let opts ← getOptions;
+let stx ← stx;
+let e ← elabTermAndSynthesize stx none <* throwErrorIfErrors;
+let stx' ← liftMetaM $ delab Name.anonymous [] e optionsPerPos;
+let stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx';
+let f' ← liftCoreM $ PrettyPrinter.formatTerm stx';
IO.println $ f'.pretty opts;
-env ← getEnv;
+let env ← getEnv;
match Parser.runParserCategory env `term (toString f') "" with
| Except.error e => throwErrorAt stx e
| Except.ok stx'' => do
- e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors;
+ let e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors;
unlessM (isDefEq e e') $
throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e')
diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean
index d4bd2ed6d0..76589dfa2a 100644
--- a/tests/lean/Process.lean
+++ b/tests/lean/Process.lean
@@ -4,27 +4,27 @@ open IO.Process
def usingIO {α} (x : IO α) : IO α := x
#eval usingIO do
- child ← spawn { cmd := "sh", args := #["-c", "exit 1"] };
+ let child ← spawn { cmd := "sh", args := #["-c", "exit 1"] };
child.wait
#eval usingIO do
- child ← spawn { cmd := "sh", args := #["-c", "echo hi!"] };
+ let child ← spawn { cmd := "sh", args := #["-c", "echo hi!"] };
child.wait
#eval usingIO do
- child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
+ let child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
child.wait;
child.stdout.readToEnd
#eval usingIO do
- child ← spawn { cmd := "head", args := #["-n1"], stdin := Stdio.piped, stdout := Stdio.piped };
+ let child ← spawn { cmd := "head", args := #["-n1"], stdin := Stdio.piped, stdout := Stdio.piped };
child.stdin.putStrLn "hu!";
child.stdin.flush;
child.wait;
child.stdout.readToEnd
#eval usingIO do
- child ← spawn { cmd := "true", stdin := Stdio.piped };
+ let child ← spawn { cmd := "true", stdin := Stdio.piped };
child.wait;
child.stdin.putStrLn "ha!";
child.stdin.flush <|> IO.println "flush of broken pipe failed"
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 3395c05bb0..77e9993b56 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -17,25 +17,25 @@ end Syntax
#eval run $ `(fun a => a) >>= pure
#eval run $ `(def foo := 1)
#eval run $ `(def foo := 1 def bar := 2)
-#eval run $ do a ← `(Nat.one); `($a)
-#eval run $ do a ← `(Nat.one); `(f $a $a)
-#eval run $ do a ← `(Nat.one); `(f $ f $a 1)
-#eval run $ do a ← `(Nat.one); `(f $(id a))
-#eval run $ do a ← `(Nat.one); `($(a).b)
-#eval run $ do a ← `(1 + 2); match_syntax a with `($a + $b) => `($b + $a) | _ => pure Syntax.missing
-#eval run $ do a ← `(def foo := 1); match_syntax a with `($f:command) => pure f | _ => pure Syntax.missing
-#eval run $ do a ← `(def foo := 1 def bar := 2); match_syntax a with `($f:command $g:command) => `($g:command $f:command) | _ => pure Syntax.missing
+#eval run $ do let a ← `(Nat.one); `($a)
+#eval run $ do let a ← `(Nat.one); `(f $a $a)
+#eval run $ do let a ← `(Nat.one); `(f $ f $a 1)
+#eval run $ do let a ← `(Nat.one); `(f $(id a))
+#eval run $ do let a ← `(Nat.one); `($(a).b)
+#eval run $ do let a ← `(1 + 2); match_syntax a with `($a + $b) => `($b + $a) | _ => pure Syntax.missing
+#eval run $ do let a ← `(def foo := 1); match_syntax a with `($f:command) => pure f | _ => pure Syntax.missing
+#eval run $ do let a ← `(def foo := 1 def bar := 2); match_syntax a with `($f:command $g:command) => `($g:command $f:command) | _ => pure Syntax.missing
-#eval run $ do a ← `(aa); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
-#eval run $ do a ← `(1 + 2); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
-#eval run $ do params ← #[`(a), `((b : Nat))].mapM id; `(fun $params* => 1)
-#eval run $ do a ← `(fun (a : Nat) b => c); match_syntax a with `(fun $aa* => $e) => pure aa | _ => pure #[]
-#eval run $ do a ← `(∀ a, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
-#eval run $ do a ← `(∀ _, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
+#eval run $ do let a ← `(aa); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
+#eval run $ do let a ← `(1 + 2); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
+#eval run $ do let params ← #[`(a), `((b : Nat))].mapM id; `(fun $params* => 1)
+#eval run $ do let a ← `(fun (a : Nat) b => c); match_syntax a with `(fun $aa* => $e) => pure aa | _ => pure #[]
+#eval run $ do let a ← `(∀ a, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
+#eval run $ do let a ← `(∀ _, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
-- this one should NOT check the kind of the matched node
-#eval run $ do a ← `(∀ _, c); match_syntax a with `(∀ $a, $e) => pure a | _ => pure a
-#eval run $ do a ← `(a); match_syntax a with `($id:ident) => pure id | _ => pure a
-#eval run $ do a ← `(a.{0}); match_syntax a with `($id:ident) => pure id | _ => pure a
-#eval run $ do a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns:matchAlt*) => pure eqns | _ => pure #[]
+#eval run $ do let a ← `(∀ _, c); match_syntax a with `(∀ $a, $e) => pure a | _ => pure a
+#eval run $ do let a ← `(a); match_syntax a with `($id:ident) => pure id | _ => pure a
+#eval run $ do let a ← `(a.{0}); match_syntax a with `($id:ident) => pure id | _ => pure a
+#eval run $ do let a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns:matchAlt*) => pure eqns | _ => pure #[]
end Lean
diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean
index 56f244df4f..c7932bf419 100644
--- a/tests/lean/ctor_layout.lean
+++ b/tests/lean/ctor_layout.lean
@@ -5,13 +5,13 @@ open Lean.IR
unsafe def main : IO Unit :=
withImportModules [{module := `Lean.Compiler.IR.Basic}] 0 fun env => do
- ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
+ let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";
- ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk;
+ let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";
- ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk;
+ let ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
pure ()
diff --git a/tests/lean/file_not_found.lean b/tests/lean/file_not_found.lean
index d1f31a6018..20f87dc7da 100644
--- a/tests/lean/file_not_found.lean
+++ b/tests/lean/file_not_found.lean
@@ -12,7 +12,7 @@ def usingIO {α} (x : IO α) := x
pure ()
#eval (discard $ IO.FS.Handle.mk "readonly.txt" Mode.write : IO Unit)
#eval usingIO do
- h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
+ let h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
h.putStr "foo";
IO.println "foo";
pure ()
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index 32a0e00f99..b3f233f929 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -1,24 +1,24 @@
new_frontend
-def inc (r : IO.Ref Nat) : IO Unit :=
-do v ← r.get;
- r.set (v+1);
- IO.println (">> " ++ toString v)
+def inc (r : IO.Ref Nat) : IO Unit := do
+let v ← r.get;
+r.set (v+1);
+IO.println (">> " ++ toString v)
def initArray (r : IO.Ref (Array Nat)) (n : Nat) : IO Unit :=
n.forM $ fun i => do
r.modify $ fun a => a.push (2*i)
-def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
-do a ← r.swap ∅;
- a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
- _ ← r.swap a;
- pure ()
+def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit := do
+let a ← r.swap ∅;
+a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
+r.swap a;
+pure ()
-def tst (n : Nat) : IO Unit :=
-do r₁ ← IO.mkRef 0;
- n.forM $ λ _ => inc r₁;
- r₂ ← IO.mkRef (∅ : Array Nat);
- initArray r₂ n;
- showArrayRef r₂
+def tst (n : Nat) : IO Unit := do
+let r₁ ← IO.mkRef 0;
+n.forM fun _ => inc r₁;
+let r₂ ← IO.mkRef (∅ : Array Nat);
+initArray r₂ n;
+showArrayRef r₂
#eval tst 10
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index 4d86d2aead..6b8658bd22 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -2,7 +2,7 @@ new_frontend
def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
catch (do modify $ fun (a : Array Nat) => a.set! 0 33;
throw "error")
- (fun _ => do a ← get; pure $ a.get! 0)
+ (fun _ => do let a ← get; pure $ a.get! 0)
def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
foo
diff --git a/tests/lean/resolveGlobalName.lean b/tests/lean/resolveGlobalName.lean
index 9384cffe84..67f75301e7 100644
--- a/tests/lean/resolveGlobalName.lean
+++ b/tests/lean/resolveGlobalName.lean
@@ -18,7 +18,7 @@ syntax[resolveKind] "#resolve " ident : command
@[commandElab resolveKind] def elabResolve : CommandElab :=
fun stx => liftTermElabM none do
- cs ← resolveGlobalName $ stx.getIdAt 1;
+ let cs ← resolveGlobalName $ stx.getIdAt 1;
Lean.Elab.logInfo $ toString cs;
pure ()
diff --git a/tests/lean/run/28.lean b/tests/lean/run/28.lean
index 4ac0a0aecb..9755771dea 100644
--- a/tests/lean/run/28.lean
+++ b/tests/lean/run/28.lean
@@ -37,8 +37,8 @@ def evalInstr : instr → sim (Option val)
| _, _ => throw (IO.userError "expected pointer value in load" )
| instr.store _ _ _ =>
- do pv <- f;
- _ <- g;
+ do let pv <- f;
+ g;
match pv with
| val.bv 27 _ => throw (IO.userError "asdf")
| _ => throw (IO.userError "expected pointer value in store" )
diff --git a/tests/lean/run/DefEqAssignBug.lean b/tests/lean/run/DefEqAssignBug.lean
index bc41a9bf2c..dff246f82d 100644
--- a/tests/lean/run/DefEqAssignBug.lean
+++ b/tests/lean/run/DefEqAssignBug.lean
@@ -12,16 +12,16 @@ unlessM x $ throwError "check failed"
def tst1 : MetaM Unit := do
let nat := mkConst `Nat;
-m1 ← mkFreshExprMVar nat;
-m2 ← mkFreshExprMVar (mkArrow nat nat);
+let m1 ← mkFreshExprMVar nat;
+let m2 ← mkFreshExprMVar (mkArrow nat nat);
withLocalDeclD `x nat $ fun x => do
let t := mkApp m2 x;
check $ isDefEq t m1
def tst2 : MetaM Unit := do
let nat := mkConst `Nat;
-m1 ← mkFreshExprMVar nat;
-m2 ← mkFreshExprMVar (mkArrow nat nat);
+let m1 ← mkFreshExprMVar nat;
+let m2 ← mkFreshExprMVar (mkArrow nat nat);
withLocalDeclD `x nat $ fun x => do
let t := mkApp m2 x;
check $ isDefEq m1 t
diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean
index c316b47c2f..e25475de58 100644
--- a/tests/lean/run/IO_test.lean
+++ b/tests/lean/run/IO_test.lean
@@ -21,22 +21,22 @@ withFile fn Mode.write fun h => do
h.write xs;
h.write xs;
pure ();
-ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
+let ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
check_eq "1" (xs.toList ++ xs.toList) ys.toList;
withFile fn Mode.append fun h => do
h.write ⟨#[5,6,7,8]⟩;
pure ();
withFile "foo.txt" Mode.read fun h => do
- ys ← h.read 10;
+ let ys ← h.read 10;
check_eq "2" [1,2,3,4,1,2,3,4,5,6] ys.toList;
- ys ← h.read 2;
+ let ys ← h.read 2;
check_eq "3" [7,8] ys.toList;
- b ← h.isEof;
+ let b ← h.isEof;
unless (!b)
(throw $ IO.userError $ "wrong (4): ");
- ys ← h.read 2;
+ let ys ← h.read 2;
check_eq "5" [] ys.toList;
- b ← h.isEof;
+ let b ← h.isEof;
unless b
(throw $ IO.userError $ "wrong (6): ");
pure ()
@@ -60,26 +60,26 @@ withFile fn2 Mode.write $ fun h => do
h.putStrLn xs₂;
h.putStrLn xs₁;
pure () };
-ys ← withFile fn2 Mode.read $ fun h => h.getLine;
+let ys ← withFile fn2 Mode.read $ fun h => h.getLine;
IO.println ys;
check_eq "1" (xs₀ ++ xs₀ ++ "\n") ys;
IO.println ys;
withFile fn2 Mode.append $ fun h => do
{ h.putStrLn xs₁;
pure () };
-ys ← withFile fn2 Mode.read $ fun h => do
- { ys ← (List.iota 4).mapM $ fun i => do
- { ln ← h.getLine;
+let ys ← withFile fn2 Mode.read $ fun h => do
+ { let ys ← (List.iota 4).mapM $ fun i => do
+ { let ln ← h.getLine;
IO.println i;
IO.println ∘ repr $ ln;
- b ← h.isEof;
+ let b ← h.isEof;
unless (i == 1 || !b) (throw $ IO.userError "isEof");
pure ln };
pure ys };
IO.println ys;
let rs := [xs₀ ++ xs₀ ++ "\n", xs₂ ++ "\n", xs₁ ++ "\n", xs₁ ++ "\n"];
check_eq "2" rs ys;
-ys ← readFile fn2;
+let ys ← readFile fn2;
check_eq "3" (String.join rs) ys;
pure ()
@@ -94,7 +94,7 @@ let xs₃ := "world";
withFile fn3 Mode.write $ fun h => do {
pure ()
};
-ys ← lines fn3;
+let ys ← lines fn3;
IO.println $ repr ys;
check_eq "1" ys #[];
withFile fn3 Mode.write $ fun h => do
@@ -102,7 +102,7 @@ withFile fn3 Mode.write $ fun h => do
h.putStrLn xs₁;
h.putStrLn xs₂;
h.putStrLn xs₃ };
-ys ← lines fn3;
+let ys ← lines fn3;
IO.println $ repr ys;
check_eq "2" ys #[xs₀, xs₁, xs₂, xs₃];
pure ()
diff --git a/tests/lean/run/LiftMethodIssue.lean b/tests/lean/run/LiftMethodIssue.lean
index 3f47de2079..a6a4bc057d 100644
--- a/tests/lean/run/LiftMethodIssue.lean
+++ b/tests/lean/run/LiftMethodIssue.lean
@@ -1,11 +1,11 @@
new_frontend
def tst : IO (Option Nat) := do
-x? : Option Nat ← pure none;
+let x? : Option Nat ← pure none;
pure x?
def tst2 (x : Nat) : IO (Option Nat) := do
-x? : Option Nat ← pure x;
+let x? : Option Nat ← pure x;
(if x?.isNone then
/-
We need the `some` because we propagate the expected type at `pure` applications.
diff --git a/tests/lean/run/Reformat.lean b/tests/lean/run/Reformat.lean
index aa57c53ea1..1831f94460 100644
--- a/tests/lean/run/Reformat.lean
+++ b/tests/lean/run/Reformat.lean
@@ -11,9 +11,9 @@ let (debug, f) : Bool × String := match args with
| [f, "-d"] => (true, f)
| [f] => (false, f)
| _ => panic! "usage: file [-d]";
-env ← mkEmptyEnvironment;
-stx ← Lean.Parser.parseFile env args.head!;
-(f, _) ← (finally (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
+let env ← mkEmptyEnvironment;
+let stx ← Lean.Parser.parseFile env args.head!;
+let (f, _) ← (finally (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
IO.print f;
--stx' ← Lean.Parser.parseModule env args.head! (toString f);
pure ()
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index 702b516ab5..953ee531fe 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -22,24 +22,24 @@ let (debug, f) : Bool × String := match args with
| [f, "-d"] => (true, f)
| [f] => (false, f)
| _ => panic! "usage: file [-d]";
-env ← mkEmptyEnvironment;
-stx ← Lean.Parser.parseFile env args.head!;
+let env ← mkEmptyEnvironment;
+let stx ← Lean.Parser.parseFile env args.head!;
let header := stx.getArg 0;
-some s ← pure header.reprint | throw $ IO.userError "header reprint failed";
+let some s ← pure header.reprint | throw $ IO.userError "header reprint failed";
IO.print s;
let cmds := (stx.getArg 1).getArgs;
cmds.forM $ fun cmd => do
let cmd := unparen cmd;
- (cmd, _) ← (finally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
- some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
+ let (cmd, _) ← (finally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
+ let some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
IO.print s
#eval main ["../../../src/Init/Core.lean"]
def check (stx : Syntax) : CoreM Unit := do
let stx' := unparen stx;
-stx' ← PrettyPrinter.parenthesizeTerm stx';
-f ← PrettyPrinter.formatTerm stx';
+let stx' ← PrettyPrinter.parenthesizeTerm stx';
+let f ← PrettyPrinter.formatTerm stx';
IO.println f;
when (stx != stx') $
throwError "reparenthesization failed"
diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean
index 2b4c36a9e0..7870e2f534 100644
--- a/tests/lean/run/bigop.lean
+++ b/tests/lean/run/bigop.lean
@@ -26,7 +26,7 @@ instance : Enumerable Bool :=
{ elems := [false, true] }
instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
-{ elems := do a ← Enumerable.elems α; b ← Enumerable.elems β; pure (a, b) }
+{ elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) }
partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
| 0, h => [⟨0, h⟩]
diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean
index a5cbf509d5..843999190f 100644
--- a/tests/lean/run/catchThe.lean
+++ b/tests/lean/run/catchThe.lean
@@ -8,7 +8,7 @@ universes u v w
abbrev M := ExceptT String $ MetaM
def testM {α} [HasBeq α] [HasToString α] (x : M α) (expected : α) : MetaM Unit := do
-r ← x;
+let r ← x;
match r with
| Except.ok a => unless (a == expected) $ throwError ("unexpected result " ++ toString a)
| Except.error e => throwError ("FAILED: " ++ e)
diff --git a/tests/lean/run/choiceExpectedTypeBug.lean b/tests/lean/run/choiceExpectedTypeBug.lean
index decf89fadb..8099a7779d 100644
--- a/tests/lean/run/choiceExpectedTypeBug.lean
+++ b/tests/lean/run/choiceExpectedTypeBug.lean
@@ -22,7 +22,7 @@ open Lean.Elab.Term
@[termElab emptyS] def elabEmptyS : TermElab :=
fun stx expectedType? => do
tryPostponeIfNoneOrMVar expectedType?;
- stxNew ← `(Nat.zero);
+ let stxNew ← `(Nat.zero);
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
def foo (x : Unit) := x
diff --git a/tests/lean/run/closure1.lean b/tests/lean/run/closure1.lean
index 4095677b76..e1dc9bc9ca 100644
--- a/tests/lean/run/closure1.lean
+++ b/tests/lean/run/closure1.lean
@@ -14,21 +14,21 @@ set_option trace.Meta.debug true
def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
def printDef (declName : Name) : MetaM Unit := do
-cinfo ← getConstInfo declName;
+let cinfo ← getConstInfo declName;
trace! `Meta.debug cinfo.value!
def tst1 : MetaM Unit := do
let u := mkLevelParam `u;
let v := mkLevelMVar `v;
-m1 ← mkFreshExprMVar (mkSort levelOne);
+let m1 ← mkFreshExprMVar (mkSort levelOne);
withLocalDeclD `α (mkSort u) $ fun α => do
withLocalDeclD `β (mkSort v) $ fun β => do
-m2 ← mkFreshExprMVar (mkArrow α m1);
+let m2 ← mkFreshExprMVar (mkArrow α m1);
withLocalDeclD `a α $ fun a => do
withLocalDeclD `f (mkArrow α α) $ fun f => do
withLetDecl `b α (mkApp f a) $ fun b => do
let t := mkApp m2 (mkApp f b);
-e ← mkAuxDefinitionFor `foo1 t;
+let e ← mkAuxDefinitionFor `foo1 t;
trace! `Meta.debug e;
printDef `foo1;
pure ()
@@ -41,11 +41,11 @@ withLocalDeclD `α (mkSort (mkLevelSucc u)) $ fun α => do
withLocalDeclD `v1 (mkApp2 (mkConst `Vec [u]) α (mkNatLit 10)) $ fun v1 =>
withLetDecl `n (mkConst `Nat) (mkNatLit 10) $ fun n =>
withLocalDeclD `v2 (mkApp2 (mkConst `Vec [u]) α n) $ fun v2 => do
-m ← mkFreshExprMVar (mkArrow (mkApp2 (mkConst `Vec [u]) α (mkNatLit 10)) (mkSort levelZero));
+let m ← mkFreshExprMVar (mkArrow (mkApp2 (mkConst `Vec [u]) α (mkNatLit 10)) (mkSort levelZero));
withLocalDeclD `p (mkSort levelZero) $ fun p => do
-t ← mkEq v1 v2;
+let t ← mkEq v1 v2;
let t := mkApp2 (mkConst `And) t (mkApp2 (mkConst `Or) (mkApp m v2) p);
-e ← mkAuxDefinitionFor `foo2 t;
+let e ← mkAuxDefinitionFor `foo2 t;
trace! `Meta.debug e;
printDef `foo2;
pure ()
diff --git a/tests/lean/run/coeIssues4.lean b/tests/lean/run/coeIssues4.lean
index 0c3bfbbb2c..b1d1866e73 100644
--- a/tests/lean/run/coeIssues4.lean
+++ b/tests/lean/run/coeIssues4.lean
@@ -2,9 +2,8 @@ new_frontend
def f : List Int → Bool := fun _ => true
-def ex3 : IO Bool :=
-do
-xs ← pure [1, 2, 3];
+def ex3 : IO Bool := do
+let xs ← pure [1, 2, 3];
pure $ f xs -- Works
inductive Expr
diff --git a/tests/lean/run/core.lean b/tests/lean/run/core.lean
index d58f0f55a3..eb66c366f1 100644
--- a/tests/lean/run/core.lean
+++ b/tests/lean/run/core.lean
@@ -3,14 +3,13 @@ new_frontend
open Lean
open Lean.Core
-def f : CoreM Nat := do {
- env ← getEnv;
- cinfo ← getConstInfo `Nat.add;
- trace! `Elab "trace message";
- liftIO $ IO.println $ toString cinfo.type;
- liftIO $ IO.println "testing...";
- pure 10
-}
+def f : CoreM Nat := do
+let env ← getEnv;
+let cinfo ← getConstInfo `Nat.add;
+trace! `Elab "trace message";
+IO.println $ toString cinfo.type;
+IO.println "testing...";
+pure 10;
#eval f
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index 97647b5624..4541c9e469 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -25,13 +25,13 @@ inductive ArrayLit3 {α : Sort u} (a b c : α) : Type u | mk : ArrayLit3 a b c
inductive ArrayLit4 {α : Sort u} (a b c d : α) : Type u | mk : ArrayLit4 a b c d
private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-env ← getEnv;
+let env ← getEnv;
match env.find? ctorName with
| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none
| _ => pure none
private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-env ← getEnv;
+let env ← getEnv;
match e with
| Expr.lit (Literal.natVal n) _ =>
if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
@@ -53,7 +53,7 @@ partial def mkPattern : Expr → MetaM Pattern
else if e.isAppOfArity `As 3 && (e.getArg! 1).isFVar then do
let v := e.getArg! 1;
let p := e.getArg! 2;
- p ← mkPattern p;
+ let p ← mkPattern p;
pure $ Pattern.as v.fvarId! p
else if e.isAppOfArity `ArrayLit0 1 ||
e.isAppOfArity `ArrayLit1 2 ||
@@ -63,64 +63,64 @@ partial def mkPattern : Expr → MetaM Pattern
let args := e.getAppArgs;
let type := args.get! 0;
let ps := args.extract 1 args.size;
- ps ← ps.toList.mapM mkPattern;
+ let ps ← ps.toList.mapM mkPattern;
pure $ Pattern.arrayLit type ps
else match e.arrayLit? with
| some (_, es) => do
- pats ← es.mapM mkPattern;
- type ← inferType e;
- type ← whnfD type;
+ let pats ← es.mapM mkPattern;
+ let type ← inferType e;
+ let type ← whnfD type;
let elemType := type.appArg!;
pure $ Pattern.arrayLit elemType pats
| none => do
- e ← whnfD e;
- r? ← constructorApp? e;
+ let e ← whnfD e;
+ let r? ← constructorApp? e;
match r? with
| none => throwError "unexpected pattern"
| some (cval, fn, args) => do
let params := args.extract 0 cval.nparams;
let fields := args.extract cval.nparams args.size;
- pats ← fields.toList.mapM mkPattern;
+ let pats ← fields.toList.mapM mkPattern;
pure $ Pattern.ctor cval.name fn.constLevels! params.toList pats
partial def decodePats : Expr → MetaM (List Pattern)
| e =>
match e.app2? `Pat with
- | some (_, pat) => do pat ← mkPattern pat; pure [pat]
+ | some (_, pat) => do let pat ← mkPattern pat; pure [pat]
| none =>
match e.prod? with
| none => throwError "unexpected pattern"
| some (pat, pats) => do
- pat ← decodePats pat;
- pats ← decodePats pats;
+ let pat ← decodePats pat;
+ let pats ← decodePats pats;
pure (pat ++ pats)
partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
forallTelescopeReducing e fun args body => do
- decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
- pats ← decodePats body;
+ let decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
+ let pats ← decodePats body;
pure { ref := Syntax.missing, fvarDecls := decls, patterns := pats }
partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
| e =>
match e.app2? `LHS with
- | some (_, lhs) => do lhs ← decodeAltLHS lhs; pure [lhs]
+ | some (_, lhs) => do let lhs ← decodeAltLHS lhs; pure [lhs]
| none =>
match e.prod? with
| none => throwError "unexpected LHS"
| some (lhs, lhss) => do
- lhs ← decodeAltLHSs lhs;
- lhss ← decodeAltLHSs lhss;
+ let lhs ← decodeAltLHSs lhs;
+ let lhss ← decodeAltLHSs lhss;
pure (lhs ++ lhss)
def withDepElimFrom {α} (declName : Name) (numPats : Nat) (k : List FVarId → List AltLHS → MetaM α) : MetaM α := do
-cinfo ← getConstInfo declName;
+let cinfo ← getConstInfo declName;
forallTelescopeReducing cinfo.type fun args body =>
if args.size < numPats then
throwError "insufficient number of parameters"
else do
let xs := (args.extract (args.size - numPats) args.size).toList.map $ Expr.fvarId!;
- alts ← decodeAltLHSs body;
+ let alts ← decodeAltLHSs body;
k xs alts
inductive LHS {α : Sort u} (a : α) : Type u
@@ -140,11 +140,11 @@ registerTraceClass `Meta.mkElim
private def getUnusedLevelParam (majors : List Expr) (lhss : List AltLHS) : MetaM Level := do
let s : CollectLevelParams.State := {};
-s ← majors.foldlM
+let s ← majors.foldlM
(fun s major => do
- major ← instantiateMVars major;
- majorType ← inferType major;
- majorType ← instantiateMVars majorType;
+ let major ← instantiateMVars major;
+ let majorType ← inferType major;
+ let majorType ← instantiateMVars majorType;
let s := collectLevelParams s major;
pure $ collectLevelParams s majorType)
s;
@@ -155,30 +155,30 @@ private def mkElimSort (majors : List Expr) (lhss : List AltLHS) (inProp : Bool)
if inProp then
pure $ mkSort $ levelZero
else do
- v ← getUnusedLevelParam majors lhss;
+ let v ← getUnusedLevelParam majors lhss;
pure $ mkSort $ v
def mkTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp : Bool := false) : MetaM MatcherResult := do
generalizeTelescope majors.toArray `_d fun majors => do
let resultType := if inProp then mkConst `True /- some proposition -/ else mkConst `Nat;
- matchType ← mkForallFVars majors resultType;
+ let matchType ← mkForallFVars majors resultType;
Match.mkMatcher elimName matchType majors.size lhss
def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
withDepElimFrom ex numPats fun majors alts => do
let majors := majors.map mkFVar;
trace! `Meta.debug ("majors: " ++ majors.toArray);
- r ← mkTester elimName majors alts inProp;
+ let r ← mkTester elimName majors alts inProp;
unless r.counterExamples.isEmpty $
throwError ("missing cases:" ++ Format.line ++ counterExamplesToMessageData r.counterExamples);
unless r.unusedAltIdxs.isEmpty $
throwError ("unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)));
- cinfo ← getConstInfo elimName;
+ let cinfo ← getConstInfo elimName;
IO.println (toString cinfo.name ++ " : " ++ toString cinfo.type);
pure ()
def testFailure (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit := do
-worked ← catch (do test ex numPats elimName inProp; pure true) (fun ex => pure false);
+let worked ← catch (do test ex numPats elimName inProp; pure true) (fun ex => pure false);
when worked $ throwError "unexpected success"
def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y)
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index 72e85bd852..660c509765 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -93,5 +93,5 @@ do
unsafe def main : IO Unit :=
do let x := Var "x";
let f := pow x x;
- _ ← nest deriv 9 f;
+ nest deriv 9 f;
pure ()
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index 4cf7035413..7043efc9be 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -16,9 +16,9 @@ p.1
set_option trace.Elab.definition true
def h (x : Nat) : StateT Nat IO Nat := do
-s ← get;
-a ← f; -- liftM inserted here
-b ← g1 1; -- liftM inserted here
+let s ← get;
+let a ← f; -- liftM inserted here
+let b ← g1 1; -- liftM inserted here
let x := g2 b;
IO.println b;
pure (s+a);
@@ -27,9 +27,9 @@ def myPrint {α} [HasToString α] (a : α) : IO Unit :=
IO.println (">> " ++ toString a)
def h₂ (x : Nat) : StateT Nat IO Nat := do
-a ← h 1; -- liftM inserted here
+let a ← h 1; -- liftM inserted here
IO.println x;
-b ← g1 a; -- liftM inserted here
+let b ← g1 a; -- liftM inserted here
when (a > 100) $ throw $ IO.userError "Error";
myPrint b.1; -- liftM inserted here
pure (a + 1)
@@ -43,9 +43,9 @@ let m2 (y : Nat) := do { -- Type inferred from application below
h (x+y); -- liftM inserted here
myPrint y -- liftM inserted here
};
-a ← h 1; -- liftM inserted here
+let a ← h 1; -- liftM inserted here
IO.println x;
-b ← g1 a; -- liftM inserted here
+let b ← g1 a; -- liftM inserted here
when (a > 100) $ throw $ IO.userError "Error";
myPrint b.1; -- liftM inserted here
m1;
@@ -53,14 +53,14 @@ m2 a;
pure 1
def tst0 : IO Unit := do {
-a ← f;
+let a ← f;
let x := a + 1;
IO.println "hello";
IO.println x;
}
def tst1 : IO Unit := do
-a ← f;
+let a ← f;
let x := a + 1;
IO.println "hello";
IO.println x;
@@ -74,8 +74,8 @@ def tst3 : IO Unit := do
(if (← g 1) > 0 then
IO.println "gt"
else do
- x ← f;
- y ← g x;
+ let x ← f;
+ let y ← g x;
IO.println y)
def pred (x : Nat) : IO Bool := do
@@ -102,13 +102,13 @@ partial def expandHash : Syntax → StateT Bool MacroM Syntax
| Syntax.node k args =>
if k == `doHash then do set true; `(←MonadState.get)
else do
- args ← args.mapM expandHash;
+ let args ← args.mapM expandHash;
pure $ Syntax.node k args;
| stx => pure stx
@[macro Lean.Parser.Term.do] def expandDo : Macro :=
fun stx => do
- (stx, expanded) ← expandHash stx false;
+ let (stx, expanded) ← expandHash stx false;
(if expanded then pure stx
else Macro.throwUnsupported)
diff --git a/tests/lean/run/elabCmd.lean b/tests/lean/run/elabCmd.lean
index 48a3ca4141..db66134b0c 100644
--- a/tests/lean/run/elabCmd.lean
+++ b/tests/lean/run/elabCmd.lean
@@ -6,7 +6,7 @@ open Lean.Elab
open Lean.Elab.Term
def getCtors (c : Name) : TermElabM (List Name) := do
-env ← getEnv;
+let env ← getEnv;
match env.find? c with
| some (ConstantInfo.inductInfo val) =>
pure val.ctors
@@ -15,10 +15,10 @@ match env.find? c with
def elabAnonCtor (args : Syntax) (τ : Expr) : TermElabM Expr := do
match τ.getAppFn with
| Expr.const C _ _ => do
- ctors ← getCtors C;
+ let ctors ← getCtors C;
match ctors with
| [c] => do
- stx ← `($(Lean.mkIdent c) $(Array.getSepElems args.getArgs)*);
+ let stx ← `($(Lean.mkIdent c) $(Array.getSepElems args.getArgs)*);
elabTerm stx τ
-- error handling
| _ => unreachable!
diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean
index 16a3ed8234..bc286b1337 100644
--- a/tests/lean/run/elab_cmd.lean
+++ b/tests/lean/run/elab_cmd.lean
@@ -6,11 +6,11 @@ open Lean.Elab.Term
open Lean.Elab.Command
elab "∃" b:term "," P:term : term => do
- ex ← `(Exists (fun $b => $P));
+ let ex ← `(Exists (fun $b => $P));
elabTerm ex none
elab "#check2" b:term : command => do
- cmd ← `(#check $b #check $b);
+ let cmd ← `(#check $b #check $b);
elabCommand cmd
#check ∃ x, x > 0
@@ -20,7 +20,7 @@ elab "#check2" b:term : command => do
#check2 10
elab "try" t:tactic : tactic => do
- t' ← `(tactic| $t <|> skip);
+ let t' ← `(tactic| $t <|> skip);
Lean.Elab.Tactic.evalTactic t'
theorem tst (x y z : Nat) : y = z → x = x → x = y → x = z :=
diff --git a/tests/lean/run/eval_unboxed_const.lean b/tests/lean/run/eval_unboxed_const.lean
index 02702f188d..2229dacb82 100644
--- a/tests/lean/run/eval_unboxed_const.lean
+++ b/tests/lean/run/eval_unboxed_const.lean
@@ -6,7 +6,7 @@ open Lean
def c1 : Bool := true
unsafe def tst1 : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
let v := env.evalConst Bool `c1;
IO.println v
@@ -15,7 +15,7 @@ IO.println v
def c2 : Bool := false
unsafe def tst2 : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
let v := env.evalConst Bool `c2;
IO.println v
diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean
index 9108ca9ff3..487d3d0d56 100644
--- a/tests/lean/run/evalconst.lean
+++ b/tests/lean/run/evalconst.lean
@@ -5,7 +5,7 @@ open Lean
def x := 10
unsafe def tst : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
IO.println $ env.evalConst Nat `x;
pure ()
@@ -14,8 +14,8 @@ pure ()
def f (x : Nat) := x + 1
unsafe def tst2 : CoreM Unit := do
-env ← getEnv;
-f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
+let env ← getEnv;
+let f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
IO.println $ (f 10);
pure ()
diff --git a/tests/lean/run/finally.lean b/tests/lean/run/finally.lean
index 60e511b806..5853e2731c 100644
--- a/tests/lean/run/finally.lean
+++ b/tests/lean/run/finally.lean
@@ -17,7 +17,7 @@ catch
(fun _ => get)
def checkE {α ε : Type} [HasBeq α] (x : IO (Except ε α)) (expected : α) : IO Unit := do
-r ← x;
+let r ← x;
match r with
| Except.ok a => unless (a == expected) $ throw $ IO.userError "unexpected result"
| Except.error _ => throw $ IO.userError "unexpected error"
@@ -47,10 +47,10 @@ catchThe IO.Error
#eval checkE ((tst3.run).run' 0) 101
def tst4 : M Nat := do
-a ← finally
+let a ← finally
(finally (pure 42) (do set 100; IO.println "inner finisher executed"; pure ()))
(do modify Nat.succ; IO.println "outer finisher executed");
-s ← get;
+let s ← get;
pure (a + s)
#eval (tst4.run).run' 0
@@ -58,13 +58,13 @@ pure (a + s)
#eval checkE ((tst4.run).run' 0) 143
def tst5 : M Nat := do
-(a, _) ← finally' (pure 42) (fun a? => do IO.println ("finalizer received: " ++ toString a?));
+let (a, _) ← finally' (pure 42) (fun a? => do IO.println ("finalizer received: " ++ toString a?));
pure a
#eval (tst5.run).run' 0
def tst6 : M Nat := do
-(a, _) ← finally' f2 (fun a? => do IO.println ("finalizer received: " ++ toString a?));
+let (a, _) ← finally' f2 (fun a? => do IO.println ("finalizer received: " ++ toString a?));
pure a
def tst7 : IO Unit :=
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 01e9f971c7..27ba91431e 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -3,14 +3,14 @@ new_frontend
open Lean
open Lean.Elab
-def run (input : String) (failIff : Bool := true) : CoreM Unit :=
-do env ← getEnv;
- opts ← getOptions;
- (env, messages) ← liftIO $ process input env opts;
- messages.forM $ fun msg => (liftIO msg.toString) >>= IO.println;
- when (failIff && messages.hasErrors) $ throwError "errors have been found";
- when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
- pure ()
+def run (input : String) (failIff : Bool := true) : CoreM Unit := do
+let env ← getEnv;
+let opts ← getOptions;
+let (env, messages) ← liftIO $ process input env opts;
+messages.forM $ fun msg => (liftIO msg.toString) >>= IO.println;
+when (failIff && messages.hasErrors) $ throwError "errors have been found";
+when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
+pure ()
def fail (input : String) : CoreM Unit :=
run input false
diff --git a/tests/lean/run/generalizeTelescope.lean b/tests/lean/run/generalizeTelescope.lean
index 29ed1b139e..c75f18be2a 100644
--- a/tests/lean/run/generalizeTelescope.lean
+++ b/tests/lean/run/generalizeTelescope.lean
@@ -18,7 +18,7 @@ let n1 := mkApp succ n;
let vecN1 := mkApp2 (mkConst `Vec) nat n1;
withLocalDeclD `xs vecN1 $ fun xs => do
generalizeTelescope #[n1, xs] `aux $ fun ys => do
-t ← mkLambdaFVars ys ys.back;
+let t ← mkLambdaFVars ys ys.back;
trace! `Meta.debug t;
pure ()
@@ -31,9 +31,9 @@ withLocalDeclD `n nat $ fun n => do
let n1 := mkApp succ n;
let vecN1 := mkApp2 (mkConst `Vec) nat n1;
withLocalDeclD `xs vecN1 $ fun xs => do
-e ← mkEqRefl xs;
+let e ← mkEqRefl xs;
generalizeTelescope #[n1, xs, e] `aux $ fun ys => do
-t ← mkLambdaFVars ys ys.back;
+let t ← mkLambdaFVars ys ys.back;
trace! `Meta.debug t;
pure ()
@@ -48,10 +48,10 @@ withLocalDeclD `n nat $ fun n => do
let n1 := mkApp succ n;
let vecN1 := mkApp2 (mkConst `Vec) nat n1;
withLocalDeclD `xs vecN1 $ fun xs => do
-e ← mkEqRefl xs;
+let e ← mkEqRefl xs;
failIfSuccess $ do {
generalizeTelescope #[n1, e] `aux $ fun ys => do
- t ← mkLambdaFVars ys ys.back;
+ let t ← mkLambdaFVars ys ys.back;
trace! `Meta.debug t;
pure ()
};
diff --git a/tests/lean/run/genindices.lean b/tests/lean/run/genindices.lean
index 6ba8fc4248..e9b42baaa0 100644
--- a/tests/lean/run/genindices.lean
+++ b/tests/lean/run/genindices.lean
@@ -11,14 +11,14 @@ open Lean
open Lean.Meta
def tst1 : MetaM Unit := do
-cinfo ← getConstInfo `goal;
+let cinfo ← getConstInfo `goal;
let type := cinfo.type;
-mvar ← mkFreshExprMVar type;
+let mvar ← mkFreshExprMVar type;
trace! `Elab (MessageData.ofGoal mvar.mvarId!);
-(_, mvarId) ← introN mvar.mvarId! 2;
-(fvarId, mvarId) ← intro1 mvarId;
+let (_, mvarId) ← introN mvar.mvarId! 2;
+let (fvarId, mvarId) ← intro1 mvarId;
trace! `Elab (MessageData.ofGoal mvarId);
-s ← generalizeIndices mvarId fvarId;
+let s ← generalizeIndices mvarId fvarId;
trace! `Elab (MessageData.ofGoal s.mvarId);
pure ()
diff --git a/tests/lean/run/getline_crash.lean b/tests/lean/run/getline_crash.lean
index 2cb3522f63..9c2d009af7 100644
--- a/tests/lean/run/getline_crash.lean
+++ b/tests/lean/run/getline_crash.lean
@@ -5,7 +5,7 @@ let path := "tmp_file";
IO.FS.withFile path IO.FS.Mode.write $ λ (h : IO.FS.Handle) =>
h.putStrLn str;
IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
- str' ← h.getLine;
+ let str' ← h.getLine;
IO.println str.length;
IO.println str'.length;
IO.print str';
@@ -20,8 +20,8 @@ IO.FS.withFile path IO.FS.Mode.write $ λ (h : IO.FS.Handle) => do {
h.putStrLn str1; h.putStr str2
};
IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
- str1' ← h.getLine;
- str2' ← h.getLine;
+ let str1' ← h.getLine;
+ let str2' ← h.getLine;
unless (str1'.length == str1.length + 1) $
throw (IO.userError ("unexpected length: " ++ toString str1'.trim.length));
unless (str1'.trim == str1) $
diff --git a/tests/lean/run/irCompilerBug.lean b/tests/lean/run/irCompilerBug.lean
index 8453085454..50f3543264 100644
--- a/tests/lean/run/irCompilerBug.lean
+++ b/tests/lean/run/irCompilerBug.lean
@@ -17,17 +17,17 @@ inductive T
@[noinline] def foo (p : Payload) : Option T :=
(do
- i ← get? p 1;
+ let i ← get? p 1;
pure (T.a i))
<|> (do
- i ← get? p 2;
+ let i ← get? p 2;
pure (T.b i))
<|> (do
- i ← get? p 3;
+ let i ← get? p 3;
pure (T.c i))
<|> (do
- i ← get? p 4;
- i ← get? p 5;
+ let i ← get? p 4;
+ let i ← get? p 5;
pure (T.d i))
def wrongOutput : String :=
diff --git a/tests/lean/run/kernel1.lean b/tests/lean/run/kernel1.lean
index c46fdafaea..a5d8f12bdc 100644
--- a/tests/lean/run/kernel1.lean
+++ b/tests/lean/run/kernel1.lean
@@ -3,7 +3,7 @@ new_frontend
open Lean
def checkDefEq (a b : Name) : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
let a := mkConst a;
let b := mkConst b;
let r := Kernel.isDefEq env {} a b;
diff --git a/tests/lean/run/kernel2.lean b/tests/lean/run/kernel2.lean
index 7dfecc23bd..f493d79c87 100644
--- a/tests/lean/run/kernel2.lean
+++ b/tests/lean/run/kernel2.lean
@@ -3,14 +3,14 @@ new_frontend
open Lean
def checkDefEq (a b : Name) : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
let a := mkConst a;
let b := mkConst b;
let r := Kernel.isDefEq env {} a b;
IO.println (toString a ++ " =?= " ++ toString b ++ " := " ++ toString r)
def whnf (a : Name) : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
let a := mkConst a;
let r := Kernel.whnf env {} a;
IO.println (toString a ++ " ==> " ++ toString r)
diff --git a/tests/lean/run/matchNoPostponing.lean b/tests/lean/run/matchNoPostponing.lean
index 24cae4fdab..69c32a9eef 100644
--- a/tests/lean/run/matchNoPostponing.lean
+++ b/tests/lean/run/matchNoPostponing.lean
@@ -6,5 +6,5 @@ new_frontend
`mkMatcher` assumes `matchType` does not contain metavariables.
We accomplish that by invoking `synthesizeSyntheticMVarsNoPostponing` at `elabMatch`. -/
def foo : IO Unit := do
-(x, y) ← pure (0, 0);
+let (x, y) ← pure (0, 0);
IO.println x
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index 5626bdbef5..738be58f53 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -5,17 +5,17 @@ open Lean.Meta
unsafe def tstInferType (mods : List Name) (e : Expr) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
- (type, _, _) ← (inferType e : MetaM _).toIO {} { env := env } {} {};
+ let (type, _, _) ← (inferType e : MetaM _).toIO {} { env := env } {} {};
IO.println (toString e ++ " : " ++ toString type)
unsafe def tstWHNF (mods : List Name) (e : Expr) (t := TransparencyMode.default) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
- (s, _, _) ← (whnf e : MetaM _).toIO {} { env := env };
+ let (s, _, _) ← (whnf e : MetaM _).toIO {} { env := env };
IO.println (toString e ++ " ==> " ++ toString s)
unsafe def tstIsProp (mods : List Name) (e : Expr) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
- (b, _, _) ← (isProp e : MetaM _).toIO {} { env := env };
+ let (b, _, _) ← (isProp e : MetaM _).toIO {} { env := env };
IO.println (toString e ++ ", isProp: " ++ toString b)
def t1 : Expr :=
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 8d9d6c1edb..2fc2b6e5cd 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -15,7 +15,7 @@ def check (x : MetaM Bool) : MetaM Unit :=
unlessM x $ throwError "check failed"
def getAssignment (m : Expr) : MetaM Expr :=
-do v? ← getExprMVarAssignment? m.mvarId!;
+do let v? ← getExprMVarAssignment? m.mvarId!;
match v? with
| some v => pure v
| none => throwError "metavariable is not assigned"
@@ -32,7 +32,7 @@ def boolTrue := mkConst `Bool.true
def tst1 : MetaM Unit :=
do print "----- tst1 -----";
- mvar ← mkFreshExprMVar nat;
+ let mvar <- mkFreshExprMVar nat;
check $ isExprDefEq mvar (mkNatLit 10);
check $ isExprDefEq mvar (mkNatLit 10);
pure ()
@@ -41,7 +41,7 @@ do print "----- tst1 -----";
def tst2 : MetaM Unit :=
do print "----- tst2 -----";
- mvar ← mkFreshExprMVar nat;
+ let mvar <- mkFreshExprMVar nat;
check $ isExprDefEq (mkApp succ mvar) (mkApp succ (mkNatLit 10));
check $ isExprDefEq mvar (mkNatLit 10);
pure ()
@@ -51,12 +51,12 @@ do print "----- tst2 -----";
def tst3 : MetaM Unit :=
do print "----- tst3 -----";
let t := mkLambda `x BinderInfo.default nat $ mkBVar 0;
- mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
+ let mvar <- mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
lambdaTelescope t fun xs _ => do
let x := xs.get! 0;
check $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
pure ();
- v ← getAssignment mvar;
+ let v <- getAssignment mvar;
print v;
pure ()
@@ -67,11 +67,11 @@ do print "----- tst4 -----";
let t := mkLambda `x BinderInfo.default nat $ mkBVar 0;
lambdaTelescope t fun xs _ => do
let x := xs.get! 0;
- mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
+ let mvar <- mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
-- the following `isExprDefEq` fails because `x` is also in the context of `mvar`
check $ not <$> isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
check $ approxDefEq $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
- v ← getAssignment mvar;
+ let v <- getAssignment mvar;
print v;
pure ();
pure ()
@@ -79,7 +79,7 @@ do print "----- tst4 -----";
#eval tst4
def mkAppC (c : Name) (xs : Array Expr) : MetaM Expr :=
-do r ← mkAppM c xs;
+do let r <- mkAppM c xs;
check r;
pure r
@@ -90,23 +90,23 @@ def mkSnd (s : Expr) : MetaM Expr := mkAppC `Prod.snd #[s]
def tst5 : MetaM Unit :=
do print "----- tst5 -----";
- p₁ ← mkPair (mkNatLit 1) (mkNatLit 2);
- x ← mkFst p₁;
+ let p₁ <- mkPair (mkNatLit 1) (mkNatLit 2);
+ let x <- mkFst p₁;
print x;
- v ← whnf x;
+ let v <- whnf x;
print v;
- v ← withTransparency TransparencyMode.reducible $ whnf x;
+ let v <- withTransparency TransparencyMode.reducible $ whnf x;
print v;
- x ← mkId x;
+ let x <- mkId x;
print x;
- prod ← mkProd nat nat;
- m ← mkFreshExprMVar prod;
- y ← mkFst m;
+ let prod <- mkProd nat nat;
+ let m <- mkFreshExprMVar prod;
+ let y <- mkFst m;
check $ isExprDefEq y x;
print y;
- x ← mkProjection p₁ `fst;
+ let x <- mkProjection p₁ `fst;
print x;
- y ← mkProjection p₁ `snd;
+ let y <- mkProjection p₁ `snd;
print y
#eval tst5
@@ -114,22 +114,22 @@ do print "----- tst5 -----";
def tst6 : MetaM Unit :=
do print "----- tst6 -----";
withLocalDeclD `x nat $ fun x => do
- m ← mkFreshExprMVar nat;
+ let m <- mkFreshExprMVar nat;
let t := mkAppN add #[m, mkNatLit 4];
let s := mkAppN add #[x, mkNatLit 3];
check $ not <$> isExprDefEq t s;
let s := mkAppN add #[x, mkNatLit 6];
check $ isExprDefEq t s;
- v ← getAssignment m;
+ let v <- getAssignment m;
check $ pure $ v == mkAppN add #[x, mkNatLit 2];
print v;
- m ← mkFreshExprMVar nat;
+ let m <- mkFreshExprMVar nat;
let t := mkAppN add #[m, mkNatLit 4];
let s := mkNatLit 3;
check $ not <$> isExprDefEq t s;
let s := mkNatLit 10;
check $ isExprDefEq t s;
- v ← getAssignment m;
+ let v <- getAssignment m;
check $ pure $ v == mkNatLit 6;
print v;
pure ()
@@ -141,15 +141,15 @@ def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
def tst7 : MetaM Unit :=
do print "----- tst7 -----";
withLocalDeclD `x type $ fun x => do
- m1 ← mkFreshExprMVar (mkArrow type type);
- m2 ← mkFreshExprMVar type;
+ let m1 <- mkFreshExprMVar (mkArrow type type);
+ let m2 <- mkFreshExprMVar type;
let t := mkApp io x;
-- we need to use foApprox to solve `?m1 ?m2 =?= IO x`
check $ not <$> isDefEq (mkApp m1 m2) t;
check $ approxDefEq $ isDefEq (mkApp m1 m2) t;
- v ← getAssignment m1;
+ let v <- getAssignment m1;
check $ pure $ v == io;
- v ← getAssignment m2;
+ let v <- getAssignment m2;
check $ pure $ v == x;
pure ()
@@ -159,11 +159,11 @@ def tst8 : MetaM Unit :=
do print "----- tst8 -----";
let add := mkAppN (mkConst `HasAdd.add [levelOne]) #[nat, mkConst `Nat.HasAdd];
let t := mkAppN add #[mkNatLit 2, mkNatLit 3];
- t ← withTransparency TransparencyMode.reducible $ whnf t;
+ let t <- withTransparency TransparencyMode.reducible $ whnf t;
print t;
- t ← whnf t;
+ let t <- whnf t;
print t;
- t ← reduce t;
+ let t <- reduce t;
print t;
pure ()
@@ -171,7 +171,7 @@ do print "----- tst8 -----";
def tst9 : MetaM Unit :=
do print "----- tst9 -----";
- env ← getEnv;
+ let env <- getEnv;
print (toString $ Lean.isReducible env `Prod.fst);
print (toString $ Lean.isReducible env `HasAdd.add);
pure ()
@@ -180,12 +180,12 @@ do print "----- tst9 -----";
def tst10 : MetaM Unit :=
do print "----- tst10 -----";
- t ← withLocalDeclD `x nat $ fun x => do {
+ let t <- withLocalDeclD `x nat $ fun x => do {
let b := mkAppN add #[x, mkAppN add #[mkNatLit 2, mkNatLit 3]];
mkLambdaFVars #[x] b
};
print t;
- t ← reduce t;
+ let t <- reduce t;
print t;
pure ()
@@ -201,8 +201,8 @@ do print "----- tst11 -----";
check $ not <$> isType x;
check $ not <$> (mkLambdaFVars #[x] x >>= isType);
check $ not <$> (mkLambdaFVars #[x] nat >>= isType);
- t ← mkEq x (mkNatLit 0);
- (t, _) ← mkForallUsedOnly #[x] t;
+ let t <- mkEq x (mkNatLit 0);
+ let (t, _) <- mkForallUsedOnly #[x] t;
print t;
check $ isType t;
pure ();
@@ -213,9 +213,9 @@ do print "----- tst11 -----";
def tst12 : MetaM Unit :=
do print "----- tst12 -----";
withLocalDeclD `x nat $ fun x => do
- t ← mkEqRefl x >>= mkLambdaFVars #[x];
+ let t <- mkEqRefl x >>= mkLambdaFVars #[x];
print t;
- type ← inferType t;
+ let type <- inferType t;
print type;
isProofQuick t >>= fun b => print (toString b);
isProofQuick nat >>= fun b => print (toString b);
@@ -227,13 +227,13 @@ do print "----- tst12 -----";
def tst13 : MetaM Unit :=
do print "----- tst13 -----";
- m₁ ← mkFreshExprMVar (mkArrow type type);
- m₂ ← mkFreshExprMVar (mkApp m₁ nat);
- t ← mkId m₂;
+ let m₁ <- mkFreshExprMVar (mkArrow type type);
+ let m₂ <- mkFreshExprMVar (mkApp m₁ nat);
+ let t <- mkId m₂;
print t;
- r ← abstractMVars t;
+ let r <- abstractMVars t;
print r.expr;
- (_, _, e) ← openAbstractMVarsResult r;
+ let (_, _, e) <- openAbstractMVarsResult r;
print e;
pure ()
@@ -246,11 +246,11 @@ def mkHasToString (a : Expr) : MetaM Expr := mkAppC `HasToString #[a]
def tst14 : MetaM Unit :=
do print "----- tst14 -----";
- stateM ← mkStateM nat;
+ let stateM <- mkStateM nat;
print stateM;
- monad ← mkMonad stateM;
- globalInsts ← getGlobalInstances;
- insts ← globalInsts.getUnify monad;
+ let monad <- mkMonad stateM;
+ let globalInsts <- getGlobalInstances;
+ let insts <- globalInsts.getUnify monad;
print insts;
pure ()
@@ -258,8 +258,8 @@ do print "----- tst14 -----";
def tst15 : MetaM Unit :=
do print "----- tst15 -----";
- inst ← mkHasAdd nat;
- r ← synthInstance inst;
+ let inst <- mkHasAdd nat;
+ let r <- synthInstance inst;
print r;
pure ()
@@ -267,10 +267,10 @@ do print "----- tst15 -----";
def tst16 : MetaM Unit :=
do print "----- tst16 -----";
- prod ← mkProd nat nat;
- inst ← mkHasToString prod;
+ let prod <- mkProd nat nat;
+ let inst <- mkHasToString prod;
print inst;
- r ← synthInstance inst;
+ let r <- synthInstance inst;
print r;
pure ()
@@ -278,11 +278,11 @@ do print "----- tst16 -----";
def tst17 : MetaM Unit :=
do print "----- tst17 -----";
- prod ← mkProd nat nat;
- prod ← mkProd boolE prod;
- inst ← mkHasToString prod;
+ let prod <- mkProd nat nat;
+ let prod <- mkProd boolE prod;
+ let inst <- mkHasToString prod;
print inst;
- r ← synthInstance inst;
+ let r <- synthInstance inst;
print r;
pure ()
@@ -290,8 +290,8 @@ do print "----- tst17 -----";
def tst18 : MetaM Unit :=
do print "----- tst18 -----";
- decEqNat ← mkDecEq nat;
- r ← synthInstance decEqNat;
+ let decEqNat <- mkDecEq nat;
+ let r <- synthInstance decEqNat;
print r;
pure ()
@@ -299,11 +299,11 @@ do print "----- tst18 -----";
def tst19 : MetaM Unit :=
do print "----- tst19 -----";
- stateM ← mkStateM nat;
+ let stateM <- mkStateM nat;
print stateM;
- monad ← mkMonad stateM;
+ let monad <- mkMonad stateM;
print monad;
- r ← synthInstance monad;
+ let r <- synthInstance monad;
print r;
pure ()
@@ -311,11 +311,11 @@ do print "----- tst19 -----";
def tst20 : MetaM Unit :=
do print "----- tst20 -----";
- stateM ← mkStateM nat;
+ let stateM <- mkStateM nat;
print stateM;
- monadState ← mkMonadState nat stateM;
+ let monadState <- mkMonadState nat stateM;
print monadState;
- r ← synthInstance monadState;
+ let r <- synthInstance monadState;
print r;
pure ()
@@ -326,21 +326,21 @@ do print "----- tst21 -----";
withLocalDeclD `x nat $ fun x => do
withLocalDeclD `y nat $ fun y => do
withLocalDeclD `z nat $ fun z => do
- eq₁ ← mkEq x y;
- eq₂ ← mkEq y z;
+ let eq₁ <- mkEq x y;
+ let eq₂ <- mkEq y z;
withLocalDeclD `h₁ eq₁ $ fun h₁ => do
withLocalDeclD `h₂ eq₂ $ fun h₂ => do
- h ← mkEqTrans h₁ h₂;
- h ← mkEqSymm h;
- h ← mkCongrArg succ h;
- h₂ ← mkEqRefl succ;
- h ← mkCongr h₂ h;
- t ← inferType h;
+ let h <- mkEqTrans h₁ h₂;
+ let h <- mkEqSymm h;
+ let h <- mkCongrArg succ h;
+ let h₂ <- mkEqRefl succ;
+ let h <- mkCongr h₂ h;
+ let t <- inferType h;
check h;
print h;
print t;
- h ← mkCongrFun h₂ x;
- t ← inferType h;
+ let h <- mkCongrFun h₂ x;
+ let t <- inferType h;
check h;
print t;
pure ()
@@ -351,11 +351,11 @@ def tst22 : MetaM Unit :=
do print "----- tst22 -----";
withLocalDeclD `x nat $ fun x => do
withLocalDeclD `y nat $ fun y => do
- t ← mkAppC `HasAdd.add #[x, y];
+ let t <- mkAppC `HasAdd.add #[x, y];
print t;
- t ← mkAppC `HasAdd.add #[y, x];
+ let t <- mkAppC `HasAdd.add #[y, x];
print t;
- t ← mkAppC `HasToString.toString #[x];
+ let t <- mkAppC `HasToString.toString #[x];
print t;
pure ()
@@ -365,7 +365,7 @@ def test1 : Nat := (fun x y => x + y) 0 1
def tst23 : MetaM Unit :=
do print "----- tst23 -----";
- cinfo ← getConstInfo `test1;
+ let cinfo <- getConstInfo `test1;
let v := cinfo.value?.get!;
print v;
print v.headBeta
@@ -374,10 +374,10 @@ do print "----- tst23 -----";
def tst24 : MetaM Unit :=
do print "----- tst24 -----";
- m1 ← mkFreshExprMVar (mkArrow nat (mkArrow type type));
- m2 ← mkFreshExprMVar type;
- zero ← mkAppM `HasZero.zero #[nat];
- idNat ← mkAppM `Id #[nat];
+ let m1 <- mkFreshExprMVar (mkArrow nat (mkArrow type type));
+ let m2 <- mkFreshExprMVar type;
+ let zero <- mkAppM `HasZero.zero #[nat];
+ let idNat <- mkAppM `Id #[nat];
let lhs := mkAppB m1 zero m2;
print zero;
print idNat;
@@ -392,19 +392,19 @@ do print "----- tst25 -----";
withLocalDeclD `α type $ fun α =>
withLocalDeclD `β type $ fun β =>
withLocalDeclD `σ type $ fun σ => do {
- (t1, n) ← mkForallUsedOnly #[α, β, σ] $ mkArrow α β;
+ let (t1, n) <- mkForallUsedOnly #[α, β, σ] $ mkArrow α β;
print t1;
check $ pure $ n == 2;
- (t2, n) ← mkForallUsedOnly #[α, β, σ] $ mkArrow α (mkArrow β σ);
+ let (t2, n) <- mkForallUsedOnly #[α, β, σ] $ mkArrow α (mkArrow β σ);
check $ pure $ n == 3;
print t2;
- (t3, n) ← mkForallUsedOnly #[α, β, σ] $ α;
+ let (t3, n) <- mkForallUsedOnly #[α, β, σ] $ α;
check $ pure $ n == 1;
print t3;
- (t4, n) ← mkForallUsedOnly #[α, β, σ] $ σ;
+ let (t4, n) <- mkForallUsedOnly #[α, β, σ] $ σ;
check $ pure $ n == 1;
print t4;
- (t5, n) ← mkForallUsedOnly #[α, β, σ] $ nat;
+ let (t5, n) <- mkForallUsedOnly #[α, β, σ] $ nat;
check $ pure $ n == 0;
print t5;
pure ()
@@ -415,11 +415,11 @@ do print "----- tst25 -----";
def tst26 : MetaM Unit := do
print "----- tst26 -----";
-m1 ← mkFreshExprMVar (mkArrow nat nat);
-m2 ← mkFreshExprMVar nat;
-m3 ← mkFreshExprMVar nat;
+let m1 <- mkFreshExprMVar (mkArrow nat nat);
+let m2 <- mkFreshExprMVar nat;
+let m3 <- mkFreshExprMVar nat;
check $ approxDefEq $ isDefEq (mkApp m1 m2) m3;
-check $ do { b ← isExprMVarAssigned $ m1.mvarId!; pure (!b) };
+check $ do { let b <- isExprMVarAssigned $ m1.mvarId!; pure (!b) };
check $ isExprMVarAssigned $ m3.mvarId!;
pure ()
@@ -435,7 +435,7 @@ set_option trace.Meta.isDefEq.assign true
def tst27 : MetaM Unit := do
print "----- tst27 -----";
-m ← mkFreshExprMVar nat;
+let m <- mkFreshExprMVar nat;
check $ isDefEq (mkNatLit 1) (mkApp (mkConst `Nat.succ) m);
pure ()
@@ -447,19 +447,19 @@ print "----- tst28 -----";
withLocalDeclD `x nat $ fun x =>
withLocalDeclD `y nat $ fun y =>
withLocalDeclD `z nat $ fun z => do
- t1 ← mkAppM `HasAdd.add #[x, y];
- t1 ← mkAppM `HasAdd.add #[x, t1];
- t1 ← mkAppM `HasAdd.add #[t1, t1];
- t2 ← mkAppM `HasAdd.add #[z, y];
- t3 ← mkAppM `Eq #[t2, t1];
- t3 ← mkForallFVars #[z] t3;
- m ← mkFreshExprMVar nat;
- p ← mkAppM `HasAdd.add #[x, m];
+ let t1 <- mkAppM `HasAdd.add #[x, y];
+ let t1 <- mkAppM `HasAdd.add #[x, t1];
+ let t1 <- mkAppM `HasAdd.add #[t1, t1];
+ let t2 <- mkAppM `HasAdd.add #[z, y];
+ let t3 <- mkAppM `Eq #[t2, t1];
+ let t3 <- mkForallFVars #[z] t3;
+ let m <- mkFreshExprMVar nat;
+ let p <- mkAppM `HasAdd.add #[x, m];
print t3;
- r ← kabstract t3 p;
+ let r <- kabstract t3 p;
print r;
- p ← mkAppM `HasAdd.add #[x, y];
- r ← kabstract t3 p;
+ let p <- mkAppM `HasAdd.add #[x, y];
+ let r <- kabstract t3 p;
print r;
pure ()
@@ -495,15 +495,15 @@ pure ()
def tst30 : MetaM Unit := do
print "----- tst30 -----";
-m1 ← mkFreshExprMVar nat;
-m2 ← mkFreshExprMVar (mkArrow nat nat);
+let m1 <- mkFreshExprMVar nat;
+let m2 <- mkFreshExprMVar (mkArrow nat nat);
withLocalDeclD `x nat $ fun x => do
let t := mkApp succ $ mkApp m2 x;
print t;
check $ approxDefEq $ isDefEq m1 t;
- r ← instantiateMVars m1;
+ let r <- instantiateMVars m1;
print r;
- r ← instantiateMVars m2;
+ let r <- instantiateMVars m2;
print r;
pure ()
@@ -511,7 +511,7 @@ withLocalDeclD `x nat $ fun x => do
def tst31 : MetaM Unit := do
print "----- tst31 -----";
-m ← mkFreshExprMVar nat;
+let m <- mkFreshExprMVar nat;
let t := mkLet `x nat zero m;
print t;
check $ isDefEq t m;
@@ -521,15 +521,15 @@ def tst32 : MetaM Unit := do
print "----- tst32 -----";
withLocalDeclD `a nat $ fun a => do
withLocalDeclD `b nat $ fun b => do
-aeqb ← mkEq a b;
+let aeqb <- mkEq a b;
withLocalDeclD `h2 aeqb $ fun h2 => do
-t ← mkEq (mkApp2 add a a) a;
+let t <- mkEq (mkApp2 add a a) a;
print t;
let motive := mkLambda `x BinderInfo.default nat (mkApp3 (mkConst `Eq [levelOne]) nat (mkApp2 add a (mkBVar 0)) a);
withLocalDeclD `h1 t $ fun h1 => do
-r ← mkEqNDRec motive h1 h2;
+let r <- mkEqNDRec motive h1 h2;
print r;
-rType ← inferType r >>= whnf;
+let rType <- inferType r >>= whnf;
print rType;
check r;
pure ()
@@ -540,17 +540,17 @@ def tst33 : MetaM Unit := do
print "----- tst33 -----";
withLocalDeclD `a nat $ fun a => do
withLocalDeclD `b nat $ fun b => do
-aeqb ← mkEq a b;
+let aeqb <- mkEq a b;
withLocalDeclD `h2 aeqb $ fun h2 => do
-t ← mkEq (mkApp2 add a a) a;
+let t <- mkEq (mkApp2 add a a) a;
let motive :=
mkLambda `x BinderInfo.default nat $
mkLambda `h BinderInfo.default (mkApp3 (mkConst `Eq [levelOne]) nat a (mkBVar 0)) $
(mkApp3 (mkConst `Eq [levelOne]) nat (mkApp2 add a (mkBVar 1)) a);
withLocalDeclD `h1 t $ fun h1 => do
-r ← mkEqRec motive h1 h2;
+let r <- mkEqRec motive h1 h2;
print r;
-rType ← inferType r >>= whnf;
+let rType <- inferType r >>= whnf;
print rType;
check r;
pure ()
@@ -561,8 +561,8 @@ def tst34 : MetaM Unit := do
print "----- tst34 -----";
let type := mkSort levelOne;
withLocalDeclD `α type $ fun α => do
- m ← mkFreshExprMVar type;
- t ← mkLambdaFVars #[α] (mkArrow m m);
+ let m <- mkFreshExprMVar type;
+ let t <- mkLambdaFVars #[α] (mkArrow m m);
print t;
pure ()
@@ -573,15 +573,15 @@ def tst35 : MetaM Unit := do
print "----- tst35 -----";
let type := mkSort levelOne;
withLocalDeclD `α type $ fun α => do
- m1 ← mkFreshExprMVar type;
- m2 ← mkFreshExprMVar (mkArrow nat type);
+ let m1 <- mkFreshExprMVar type;
+ let m2 <- mkFreshExprMVar (mkArrow nat type);
let v := mkLambda `x BinderInfo.default nat m1;
assignExprMVar m2.mvarId! v;
let w := mkApp m2 zero;
- t1 ← mkLambdaFVars #[α] (mkArrow w w);
+ let t1 <- mkLambdaFVars #[α] (mkArrow w w);
print t1;
- m3 ← mkFreshExprMVar type;
- t2 ← mkLambdaFVars #[α] (mkArrow (mkBVar 0) (mkBVar 1));
+ let m3 <- mkFreshExprMVar type;
+ let t2 <- mkLambdaFVars #[α] (mkArrow (mkBVar 0) (mkBVar 1));
print t2;
check $ isDefEq t1 t2;
pure ()
@@ -592,10 +592,10 @@ withLocalDeclD `α type $ fun α => do
def tst36 : MetaM Unit := do
print "----- tst36 -----";
let type := mkSort levelOne;
-m1 ← mkFreshExprMVar (mkArrow type type);
+let m1 <- mkFreshExprMVar (mkArrow type type);
withLocalDeclD `α type $ fun α => do
- m2 ← mkFreshExprMVar type;
- t ← mkAppM `Id #[m2];
+ let m2 <- mkFreshExprMVar type;
+ let t <- mkAppM `Id #[m2];
check $ approxDefEq $ isDefEq (mkApp m1 α) t;
check $ approxDefEq $ isDefEq m1 (mkConst `Id [levelZero]);
pure ()
@@ -604,11 +604,11 @@ withLocalDeclD `α type $ fun α => do
def tst37 : MetaM Unit := do
print "----- tst37 -----";
-m1 ← mkFreshExprMVar (mkArrow nat (mkArrow type type));
-m2 ← mkFreshExprMVar (mkArrow nat type);
+let m1 <- mkFreshExprMVar (mkArrow nat (mkArrow type type));
+let m2 <- mkFreshExprMVar (mkArrow nat type);
withLocalDeclD `v nat $ fun v => do
let lhs := mkApp2 m1 v (mkApp m2 v);
- rhs ← mkAppM `StateM #[nat, nat];
+ let rhs <- mkAppM `StateM #[nat, nat];
print lhs;
print rhs;
check $ approxDefEq $ isDefEq lhs rhs;
@@ -618,11 +618,11 @@ withLocalDeclD `v nat $ fun v => do
def tst38 : MetaM Unit := do
print "----- tst38 -----";
-m1 ← mkFreshExprMVar nat;
+let m1 <- mkFreshExprMVar nat;
withLocalDeclD `x nat $ fun x => do
-m2 ← mkFreshExprMVar type;
+let m2 <- mkFreshExprMVar type;
withLocalDeclD `y m2 $ fun y => do
-m3 ← mkFreshExprMVar (mkArrow m2 nat);
+let m3 <- mkFreshExprMVar (mkArrow m2 nat);
let rhs := mkApp m3 y;
check $ approxDefEq $ isDefEq m2 nat;
print m2;
@@ -643,10 +643,10 @@ def tst39 : MetaM Unit := do
print "----- tst39 -----";
withLocalDeclD `α type $ fun α =>
withLocalDeclD `β type $ fun β => do
- p ← mkProd α β;
- t ← mkForallFVars #[α, β] p;
+ let p <- mkProd α β;
+ let t <- mkForallFVars #[α, β] p;
print t;
- e ← instantiateForall t #[nat, boolE];
+ let e <- instantiateForall t #[nat, boolE];
print e;
pure ()
@@ -660,9 +660,9 @@ withLocalDeclD `β type $ fun β =>
withLocalDeclD `a α $ fun a =>
withLocalDeclD `b β $ fun b =>
do
- p ← mkProd α β;
- t1 ← mkForallFVars #[α, β] p;
- t2 ← mkForallFVars #[α, β, a, b] p;
+ let p <- mkProd α β;
+ let t1 <- mkForallFVars #[α, β] p;
+ let t2 <- mkForallFVars #[α, β, a, b] p;
print t1;
print $ toString $ t1.bindingBody!.hasLooseBVarInExplicitDomain 0 false;
print $ toString $ t1.bindingBody!.hasLooseBVarInExplicitDomain 0 true;
@@ -697,24 +697,24 @@ structure C (α : Type u) extends A α, B α :=
def mkA (x y : Expr) : MetaM Expr := mkAppC `A.mk #[x, y]
def mkB (z : Expr) : MetaM Expr := mkAppC `B.mk #[z]
def mkC (x y z w : Expr) : MetaM Expr := do
-a ← mkA x y;
-b ← mkB z;
+let a <- mkA x y;
+let b <- mkB z;
mkAppC `C.mk #[a, b, w]
def tst41 : MetaM Unit := do
print "----- tst41 -----";
-c ← mkC (mkNatLit 1) (mkNatLit 2) (mkNatLit 3) boolTrue;
+let c <- mkC (mkNatLit 1) (mkNatLit 2) (mkNatLit 3) boolTrue;
print c;
-x ← mkProjection c `x;
+let x <- mkProjection c `x;
check x;
print x;
-y ← mkProjection c `y;
+let y <- mkProjection c `y;
check y;
print y;
-z ← mkProjection c `z;
+let z <- mkProjection c `z;
check z;
print z;
-w ← mkProjection c `w;
+let w <- mkProjection c `w;
check w;
print w;
pure ()
@@ -728,10 +728,10 @@ set_option pp.all false
def tst42 : MetaM Unit := do
print "----- tst42 -----";
-t ← mkListLit nat [mkNatLit 1, mkNatLit 2];
+let t <- mkListLit nat [mkNatLit 1, mkNatLit 2];
print t;
check t;
-t ← mkArrayLit nat [mkNatLit 1, mkNatLit 2];
+let t <- mkArrayLit nat [mkNatLit 1, mkNatLit 2];
print t;
check t;
match t.arrayLit? with
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index a2e984a447..afadbbec01 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -16,7 +16,7 @@ def check (x : MetaM Bool) : MetaM Unit :=
unlessM x $ throwError "check failed"
def getAssignment (m : Expr) : MetaM Expr :=
-do v? ← getExprMVarAssignment? m.mvarId!;
+do let v? ← getExprMVarAssignment? m.mvarId!;
match v? with
| some v => pure v
| none => throwError "metavariable is not assigned"
@@ -24,7 +24,7 @@ do v? ← getExprMVarAssignment? m.mvarId!;
unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
let x : MetaM Unit := do { x; printTraces };
- _ ← x.toIO { options := opts } { env := env };
+ x.toIO { options := opts } { env := env };
pure ()
def nat := mkConst `Nat
@@ -33,26 +33,26 @@ def add := mkAppN (mkConst `HasAdd.add [levelZero]) #[nat, mkConst `Nat.HasAdd]
def tst1 : MetaM Unit :=
do let d : DiscrTree Nat := {};
- mvar ← mkFreshExprMVar nat;
- d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
- d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;
- d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3;
- d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4;
- d ← d.insert mvar 5;
+ let mvar ← mkFreshExprMVar nat;
+ let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
+ let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;
+ let d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3;
+ let d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4;
+ let d ← d.insert mvar 5;
print (format d);
- vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
+ let vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
print (format vs);
let t := mkAppN add #[mvar, mvar];
print t;
- vs ← d.getMatch t;
+ let vs ← d.getMatch t;
print (format vs);
- vs ← d.getUnify t;
+ let vs ← d.getUnify t;
print (format vs);
- vs ← d.getUnify mvar;
+ let vs ← d.getUnify mvar;
print (format vs);
- vs ← d.getUnify $ mkAppN add #[mkNatLit 0, mvar];
+ let vs ← d.getUnify $ mkAppN add #[mkNatLit 0, mvar];
print (format vs);
- vs ← d.getUnify $ mkAppN add #[mvar, mkNatLit 20];
+ let vs ← d.getUnify $ mkAppN add #[mvar, mkNatLit 20];
print (format vs);
pure ()
diff --git a/tests/lean/run/meta4.lean b/tests/lean/run/meta4.lean
index 0490721c2c..32f3524e77 100644
--- a/tests/lean/run/meta4.lean
+++ b/tests/lean/run/meta4.lean
@@ -14,23 +14,23 @@ axiom Ax : forall (α β : Type), α → β → DecidableEq β
set_option trace.Meta.debug true
def tst1 : MetaM Unit := do
-cinfo ← getConstInfo `Ax;
-(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 0);
+let cinfo ← getConstInfo `Ax;
+let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 0);
check (pure (!e.hasMVar));
print e;
-(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 1);
+let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 1);
check (pure e.hasMVar);
check (pure e.isForall);
print e;
-(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 5);
+let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 5);
check (pure e.hasMVar);
check (pure e.isForall);
print e;
-(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 6);
+let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 6);
check (pure e.hasMVar);
check (pure (!e.isForall));
print e;
-(_, _, e') ← forallMetaTelescopeReducing cinfo.type;
+let (_, _, e') ← forallMetaTelescopeReducing cinfo.type;
print e';
check (isDefEq e e');
forallBoundedTelescope cinfo.type (some 0) $ fun xs body => check (pure (xs.size == 0));
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
index 8fc930e09d..0d338d5b67 100644
--- a/tests/lean/run/meta5.lean
+++ b/tests/lean/run/meta5.lean
@@ -6,15 +6,15 @@ open Lean.Meta
def tst1 : MetaM Unit :=
withLocalDeclD `y (mkConst `Nat) $ fun y => do
withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
- mvar ← mkFreshExprMVar (mkConst `Nat) MetavarKind.syntheticOpaque;
+ let mvar ← mkFreshExprMVar (mkConst `Nat) MetavarKind.syntheticOpaque;
trace! `Meta mvar;
- r ← mkLambdaFVars #[y, x] mvar;
+ let r ← mkLambdaFVars #[y, x] mvar;
trace! `Meta r;
let v := mkApp2 (mkConst `Nat.add) x y;
assignExprMVar mvar.mvarId! v;
trace! `Meta mvar;
trace! `Meta r;
- mctx ← getMCtx;
+ let mctx ← getMCtx;
mctx.decls.forM $ fun mvarId mvarDecl => do {
trace! `Meta ("?" ++ mvarId ++ " : " ++ mvarDecl.type);
pure ()
diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean
index b16907fee5..97ad62b4ad 100644
--- a/tests/lean/run/meta6.lean
+++ b/tests/lean/run/meta6.lean
@@ -20,7 +20,7 @@ def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
def tst1 : MetaM Unit := do
print "----- tst1 -----";
-m1 ← mkFreshExprMVar (mkArrow nat nat);
+let m1 ← mkFreshExprMVar (mkArrow nat nat);
let lhs := mkApp m1 zero;
let rhs := zero;
check $ fullApproxDefEq $ isDefEq lhs rhs;
@@ -34,9 +34,9 @@ set_option trace.Meta.debug true
def tst2 : MetaM Unit := do
print "----- tst2 -----";
-ps ← getParamNames `Or.elim; print (toString ps);
-ps ← getParamNames `Iff.elim; print (toString ps);
-ps ← getParamNames `check; print (toString ps);
+let ps ← getParamNames `Or.elim; print (toString ps);
+let ps ← getParamNames `Iff.elim; print (toString ps);
+let ps ← getParamNames `check; print (toString ps);
pure ()
#eval tst2
@@ -45,17 +45,17 @@ axiom t1 : [Unit] = []
axiom t2 : 0 > 5
def tst3 : MetaM Unit := do
-env ← getEnv;
-t2 ← getConstInfo `t2;
-c ← mkNoConfusion t2.type (mkConst `t1);
+let env ← getEnv;
+let t2 ← getConstInfo `t2;
+let c ← mkNoConfusion t2.type (mkConst `t1);
print c;
Meta.check c;
-cType ← inferType c;
+let cType ← inferType c;
print cType;
-lt ← mkLt (mkNatLit 10000000) (mkNatLit 20000000000);
-ltPrf ← mkDecideProof lt;
+let lt ← mkLt (mkNatLit 10000000) (mkNatLit 20000000000);
+let ltPrf ← mkDecideProof lt;
Meta.check ltPrf;
-t ← inferType ltPrf;
+let t ← inferType ltPrf;
print t;
pure ()
@@ -68,15 +68,15 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
def tst4 : MetaM Unit :=
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
-vType ← mkAppM `Vec #[nat, x];
+let vType ← mkAppM `Vec #[nat, x];
withLocalDeclD `v vType fun v => do
-m ← mkFreshExprSyntheticOpaqueMVar vType;
-subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
+let m ← mkFreshExprSyntheticOpaqueMVar vType;
+let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
subgoals.forM fun s => do {
print (MessageData.ofGoal s.mvarId);
assumption s.mvarId
};
-t ← instantiateMVars m;
+let t ← instantiateMVars m;
print t;
Meta.check t;
pure ()
@@ -84,14 +84,14 @@ pure ()
#eval tst4
def tst5 : MetaM Unit := do
-arrayNat ← mkAppM `Array #[nat];
+let arrayNat ← mkAppM `Array #[nat];
withLocalDeclD `a arrayNat fun a => do
withLocalDeclD `b arrayNat fun b => do
let motiveType := _root_.mkArrow arrayNat (mkSort levelZero);
withLocalDeclD `motive motiveType fun motive => do
let mvarType := mkApp motive a;
-mvar ← mkFreshExprSyntheticOpaqueMVar mvarType;
-subgoals ← caseArraySizes mvar.mvarId! a.fvarId! #[1, 0, 4, 5];
+let mvar ← mkFreshExprSyntheticOpaqueMVar mvarType;
+let subgoals ← caseArraySizes mvar.mvarId! a.fvarId! #[1, 0, 4, 5];
subgoals.forM fun s => do {
print (MessageData.ofGoal s.mvarId);
pure ()
diff --git a/tests/lean/run/meta7.lean b/tests/lean/run/meta7.lean
index f8628bd122..51313b08b5 100644
--- a/tests/lean/run/meta7.lean
+++ b/tests/lean/run/meta7.lean
@@ -26,15 +26,15 @@ let z := f 10;
def tst1 : MetaM Unit := do
print "----- tst1 -----";
-c ← getConstInfo `ex;
+let c ← getConstInfo `ex;
lambdaTelescope c.value?.get! fun xs body =>
withTrackingZeta do
Meta.check body;
- ys ← getZetaFVarIds;
+ let ys ← getZetaFVarIds;
let ys := ys.toList.map mkFVar;
print ys;
check $ pure $ ys.length == 2;
- c ← mkAuxDefinitionFor `foo body;
+ let c ← mkAuxDefinitionFor `foo body;
print c;
Meta.check c;
pure ()
@@ -79,10 +79,10 @@ print "----- tst4 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
-m ← mkFreshExprMVar nat;
+let m ← mkFreshExprMVar nat;
print (← ppGoal m.mvarId!);
-val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
-⟨zId, nId, subst⟩ ← assertAfter m.mvarId! x.fvarId! `z nat val;
+let val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
+let ⟨zId, nId, subst⟩ ← assertAfter m.mvarId! x.fvarId! `z nat val;
print m;
print (← ppGoal nId);
withMVarContext nId do {
@@ -91,7 +91,7 @@ withMVarContext nId do {
print (mkMVar nId)
};
print m;
-expected ← mkAppM `HasAdd.add #[x, val];
+let expected ← mkAppM `HasAdd.add #[x, val];
check (isDefEq m expected);
pure ()
@@ -103,10 +103,10 @@ let prop := mkSort levelZero;
withLocalDeclD `p prop fun p =>
withLocalDeclD `q prop fun q => do
withLocalDeclD `h₁ p fun h₁ => do
-eq ← mkEq p q;
+let eq ← mkEq p q;
withLocalDeclD `h₂ eq fun h₂ => do
-m ← mkFreshExprMVar q;
-r ← replaceLocalDecl m.mvarId! h₁.fvarId! q h₂;
+let m ← mkFreshExprMVar q;
+let r ← replaceLocalDecl m.mvarId! h₁.fvarId! q h₂;
print (← ppGoal r.mvarId);
assignExprMVar r.mvarId (mkFVar r.fvarId);
print m;
@@ -120,10 +120,10 @@ print "----- tst6 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
-m ← mkFreshExprMVar nat;
+let m ← mkFreshExprMVar nat;
print (← ppGoal m.mvarId!);
-val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
-⟨zId, nId, subst⟩ ← assertAfter m.mvarId! y.fvarId! `z nat val;
+let val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
+let ⟨zId, nId, subst⟩ ← assertAfter m.mvarId! y.fvarId! `z nat val;
print m;
print (← ppGoal nId);
withMVarContext nId do {
@@ -132,7 +132,7 @@ withMVarContext nId do {
print (mkMVar nId)
};
print m;
-expected ← mkAppM `HasAdd.add #[x, val];
+let expected ← mkAppM `HasAdd.add #[x, val];
check (isDefEq m expected);
pure ()
@@ -143,11 +143,11 @@ print "----- tst7 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
-val ← mkAppM `HasAdd.add #[x, y];
+let val ← mkAppM `HasAdd.add #[x, y];
print val;
let val := val.replaceFVars #[x, y] #[mkNatLit 0, mkNatLit 1];
print val;
-expected ← mkAppM `HasAdd.add #[mkNatLit 0, mkNatLit 1];
+let expected ← mkAppM `HasAdd.add #[mkNatLit 0, mkNatLit 1];
print expected;
check (pure $ val == expected);
pure ()
diff --git a/tests/lean/run/monadCache.lean b/tests/lean/run/monadCache.lean
index b2213cbfdf..4d0c071fb8 100644
--- a/tests/lean/run/monadCache.lean
+++ b/tests/lean/run/monadCache.lean
@@ -11,7 +11,7 @@ partial def depth : Expr → MonadCacheT Expr Nat CoreM Nat
checkCache e fun e =>
match e with
| Expr.const c [] _ => pure 1
- | Expr.app f a _ => do d₁ ← depth f; d₂ ← depth a; pure $ Nat.max d₁ d₂ + 1
+ | Expr.app f a _ => do pure $ Nat.max (← depth f) (← depth a) + 1
| _ => pure 0
#eval (depth (mkTower 100)).run
@@ -27,7 +27,7 @@ partial def visit : Expr → MonadCacheT Expr Expr CoreM Expr
#eval (visit (mkTower 4)).run
def tst : CoreM Nat := do
-e ← (visit (mkTower 100)).run; (depth e).run
+let e ← (visit (mkTower 100)).run; (depth e).run
#eval tst
@@ -47,6 +47,6 @@ e.forEach fun e => match e with
| _ => pure ()
def tst2 : CoreM Unit := do
-e ← (visit (mkTower 100)).run; displayConsts e
+let e ← (visit (mkTower 100)).run; displayConsts e
#eval tst2
diff --git a/tests/lean/run/monadControl.lean b/tests/lean/run/monadControl.lean
index 323484ffbf..ffc53982d8 100644
--- a/tests/lean/run/monadControl.lean
+++ b/tests/lean/run/monadControl.lean
@@ -3,7 +3,7 @@ new_frontend
@[inline] def f {α} (s : String) (x : IO α) : IO α := do
IO.println "started";
IO.println s;
-a ← x;
+let a ← x;
IO.println ("ended");
pure a
@@ -13,7 +13,7 @@ controlAt IO fun runInBase => f msg (runInBase x)
abbrev M := StateT Bool $ ExceptT String $ StateT String $ ReaderT Nat $ StateT Nat IO
def tst : M Nat := do
-a ← f'' "hello" do { s ← getThe Nat; ctx ← read; modifyThe Nat fun s => s + ctx; when (s > 10) $ throw "ERROR"; getThe Nat };
+let a ← f'' "hello" do { let s ← getThe Nat; let ctx ← read; modifyThe Nat fun s => s + ctx; when (s > 10) $ throw "ERROR"; getThe Nat };
modifyThe Nat Nat.succ;
pure a
@@ -22,7 +22,7 @@ pure a
@[inline] def g {α} (s : String) (x : Nat → IO α) : IO α := do
IO.println "started";
IO.println s;
-a ← x s.length;
+let a ← x s.length;
IO.println ("ended");
pure a
@@ -30,7 +30,7 @@ pure a
controlAt IO fun runInBase => g msg (fun n => runInBase (x n))
def tst2 : M Nat := do
-a ← g' "hello" fun x => do { s ← getThe Nat; ctx ← read; modifyThe Nat fun s => s + ctx + x; when (s > 10) $ throw "ERROR"; getThe Nat };
+let a ← g' "hello" fun x => do { let s ← getThe Nat; let ctx ← read; modifyThe Nat fun s => s + ctx + x; when (s > 10) $ throw "ERROR"; getThe Nat };
modifyThe Nat Nat.succ;
pure a
diff --git a/tests/lean/run/nicerNestedDos.lean b/tests/lean/run/nicerNestedDos.lean
index ebe1ac4004..35776916a2 100644
--- a/tests/lean/run/nicerNestedDos.lean
+++ b/tests/lean/run/nicerNestedDos.lean
@@ -12,7 +12,7 @@ pure (x + 1)
def g (x : Nat) : StateT Nat Id Unit := do
when (x > 10) do
- s ← get;
+ let s ← get;
set (s + x);
pure ()
@@ -24,7 +24,7 @@ rfl
def h (x : Nat) : StateT Nat Id Unit := do
when (x > 10) do {
- s ← get;
+ let s ← get;
set (s + x) -- we don't need to respect indentation when `{` `}` are used
};
pure ()
diff --git a/tests/lean/run/parseCore.lean b/tests/lean/run/parseCore.lean
index 16eff8c406..58b57c19d4 100644
--- a/tests/lean/run/parseCore.lean
+++ b/tests/lean/run/parseCore.lean
@@ -4,8 +4,8 @@ def test : IO Unit :=
if System.Platform.isWindows then
pure () -- TODO investigate why the following doesn't work on Windows
else do
- env ← Lean.mkEmptyEnvironment;
- _ ← Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]);
+ let env ← Lean.mkEmptyEnvironment;
+ Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]);
IO.println "done"
#eval test
diff --git a/tests/lean/run/quasi_pattern_unification_approx_issue.lean b/tests/lean/run/quasi_pattern_unification_approx_issue.lean
index 507e179e6f..c572ce13a7 100644
--- a/tests/lean/run/quasi_pattern_unification_approx_issue.lean
+++ b/tests/lean/run/quasi_pattern_unification_approx_issue.lean
@@ -8,6 +8,6 @@ getThe σ
def foo1 : StateT δ (StateT σ Id) σ :=
monadLift (get : StateT σ Id σ)
-def foo2 : StateT δ (StateT σ Id) σ :=
-do s : σ ← monadLift (get : StateT σ Id σ);
- pure s
+def foo2 : StateT δ (StateT σ Id) σ := do
+let s : σ ← monadLift (get : StateT σ Id σ);
+pure s
diff --git a/tests/lean/run/readerThe.lean b/tests/lean/run/readerThe.lean
index 435da94531..30e3dc6dcc 100644
--- a/tests/lean/run/readerThe.lean
+++ b/tests/lean/run/readerThe.lean
@@ -4,11 +4,11 @@ abbrev M := ReaderT String $ StateT Nat $ ReaderT Bool $ IO
def f : M Nat := do
-s ← read;
+let s ← read;
IO.println s;
-b ← readThe Bool;
+let b ← readThe Bool;
IO.println b;
-s ← get;
+let s ← get;
pure s
#eval (f "hello").run' 10 true
diff --git a/tests/lean/run/recInfo1.lean b/tests/lean/run/recInfo1.lean
index 81f30b78f5..9190654c51 100644
--- a/tests/lean/run/recInfo1.lean
+++ b/tests/lean/run/recInfo1.lean
@@ -7,7 +7,7 @@ def print (msg : MessageData) : MetaM Unit :=
trace! `Meta.debug msg
def showRecInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM Unit := do
-info ← mkRecursorInfo declName majorPos?;
+let info ← mkRecursorInfo declName majorPos?;
print (toString info)
set_option trace.Meta true
diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean
index 6f4dbd5404..86b7e45df2 100644
--- a/tests/lean/run/sharecommon.lean
+++ b/tests/lean/run/sharecommon.lean
@@ -8,11 +8,11 @@ unsafe def tst1 : ShareCommonT IO Unit := do
let x := [1];
let y := [0].map (fun x => x + 1);
check $ ptrAddrUnsafe x != ptrAddrUnsafe y;
-x ← shareCommonM x;
-y ← shareCommonM y;
+let x ← shareCommonM x;
+let y ← shareCommonM y;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
-z ← shareCommonM [2];
-x ← shareCommonM x;
+let z ← shareCommonM [2];
+let x ← shareCommonM x;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
check $ ptrAddrUnsafe x != ptrAddrUnsafe z;
IO.println x;
@@ -25,11 +25,11 @@ unsafe def tst2 : ShareCommonT IO Unit := do
let x := [1, 2];
let y := [0, 1].map (fun x => x + 1);
check $ ptrAddrUnsafe x != ptrAddrUnsafe y;
-x ← shareCommonM x;
-y ← shareCommonM y;
+let x ← shareCommonM x;
+let y ← shareCommonM y;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
-z ← shareCommonM [2];
-x ← shareCommonM x;
+let z ← shareCommonM [2];
+let x ← shareCommonM x;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
check $ ptrAddrUnsafe x != ptrAddrUnsafe z;
IO.println x;
@@ -52,9 +52,9 @@ let o2 := mkFoo2 10 true;
let o3 := mkFoo2 10 false;
check $ ptrAddrUnsafe o1 != ptrAddrUnsafe o2;
check $ ptrAddrUnsafe o1 != ptrAddrUnsafe o3;
-o1 ← shareCommonM o1;
-o2 ← shareCommonM o2;
-o3 ← shareCommonM o3;
+let o1 ← shareCommonM o1;
+let o2 ← shareCommonM o2;
+let o3 ← shareCommonM o3;
check $
o1.x == 10 && o1.y == true &&
o1.z == true && o3.z == false &&
@@ -69,11 +69,11 @@ unsafe def tst4 : ShareCommonT IO Unit := do
let x := ["hello"];
let y := ["ello"].map (fun x => "h" ++ x);
check $ ptrAddrUnsafe x != ptrAddrUnsafe y;
-x ← shareCommonM x;
-y ← shareCommonM y;
+let x ← shareCommonM x;
+let y ← shareCommonM y;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
-z ← shareCommonM ["world"];
-x ← shareCommonM x;
+let z ← shareCommonM ["world"];
+let x ← shareCommonM x;
check $
ptrAddrUnsafe x == ptrAddrUnsafe y &&
ptrAddrUnsafe x != ptrAddrUnsafe z;
@@ -104,9 +104,9 @@ check $
ptrAddrUnsafe (a.get! 0) != ptrAddrUnsafe (a.get! 2) &&
ptrAddrUnsafe (b.get! 0) != ptrAddrUnsafe (b.get! 1) &&
ptrAddrUnsafe (c.get! 0) != ptrAddrUnsafe (c.get! 1);
-a ← shareCommonM a;
-b ← shareCommonM b;
-c ← shareCommonM c;
+let a ← shareCommonM a;
+let b ← shareCommonM b;
+let c ← shareCommonM c;
check $
ptrAddrUnsafe a == ptrAddrUnsafe b &&
ptrAddrUnsafe a != ptrAddrUnsafe c &&
@@ -137,9 +137,9 @@ IO.println b;
IO.println c;
check $ ptrAddrUnsafe a != ptrAddrUnsafe b;
check $ ptrAddrUnsafe a != ptrAddrUnsafe c;
-a ← shareCommonM a;
-b ← shareCommonM b;
-c ← shareCommonM c;
+let a ← shareCommonM a;
+let b ← shareCommonM b;
+let c ← shareCommonM c;
check $ ptrAddrUnsafe a == ptrAddrUnsafe b;
check $ ptrAddrUnsafe a != ptrAddrUnsafe c;
pure ()
diff --git a/tests/lean/run/spec_issue.lean b/tests/lean/run/spec_issue.lean
index 7d22a44949..a3e04cbe71 100644
--- a/tests/lean/run/spec_issue.lean
+++ b/tests/lean/run/spec_issue.lean
@@ -3,5 +3,5 @@ set_option trace.compiler.ir.result true
def g (ys : List Nat) : IO Nat := do
let x := 0;
-(_, x) ← StateT.run (ys.forM fun y => IO.println y) x;
+let (_, x) ← StateT.run (ys.forM fun y => IO.println y) x;
pure x
diff --git a/tests/lean/run/stateRef.lean b/tests/lean/run/stateRef.lean
index 355dd314ac..21e371052e 100644
--- a/tests/lean/run/stateRef.lean
+++ b/tests/lean/run/stateRef.lean
@@ -13,7 +13,7 @@ def g : IO Nat :=
#eval (do set 100; f 5 : StateRefT Nat IO Nat).run' 0
def f2 : ReaderT Nat (StateRefT Nat IO) Nat := do
-v ← read;
+let v ← read;
IO.println $ "context " ++ toString v;
modify fun s => s + v;
get
@@ -21,10 +21,10 @@ get
#eval (f2.run 10).run' 20
def f3 : StateT String (StateRefT Nat IO) Nat := do
-s ← get;
-n ← getThe Nat;
+let s ← get;
+let n ← getThe Nat;
set (s ++ ", " ++ toString n);
-s ← get;
+let s ← get;
IO.println s;
set (n+1);
getThe Nat
@@ -38,16 +38,16 @@ class HasGetAt {β : Type} (v : β) (α : outParam Type) (m : Type → Type) :=
(getAt : m α)
instance monadState.hasGetAt (β : Type) (v : β) (α : Type) (m : Type → Type) [Monad m] [MonadStateOf (Label v α) m] : HasGetAt v α m :=
-{ getAt := do a ← getThe (Label v α); pure a.val }
+{ getAt := do let a ← getThe (Label v α); pure a.val }
export HasGetAt (getAt)
abbrev M := StateRefT (Label 0 Nat) $ StateRefT (Label 1 Nat) $ StateRefT (Label 2 Nat) IO
def f4 : M Nat := do
-a0 : Nat ← getAt 0;
-a1 ← getAt 1;
-a2 ← getAt 2;
+let a0 : Nat ← getAt 0;
+let a1 ← getAt 1;
+let a2 ← getAt 2;
IO.println $ "state0 " ++ toString a0;
IO.println $ "state1 " ++ toString a1;
IO.println $ "state1 " ++ toString a2;
@@ -58,7 +58,7 @@ pure (a0 + a1 + a2)
abbrev S (ω : Type) := StateRefT Nat $ StateRefT String $ ST ω
def f5 {ω} : S ω Unit := do
-s ← getThe String;
+let s ← getThe String;
modify fun n => n + s.length;
pure ()
diff --git a/tests/lean/run/strInterpolation.lean b/tests/lean/run/strInterpolation.lean
index 958871a115..8be2245a07 100644
--- a/tests/lean/run/strInterpolation.lean
+++ b/tests/lean/run/strInterpolation.lean
@@ -87,7 +87,7 @@ let rec loop (i : String.Pos) (acc : String) :=
else if s.atEnd i then
none
else if c == '\\' then do
- (c, i) ← decodeStrInterpolantQuotedChar s i;
+ let (c, i) ← decodeStrInterpolantQuotedChar s i;
loop i (acc.push c)
else
loop i (acc.push c);
@@ -100,7 +100,7 @@ match isLit? Parser.strInterpolantStrLitKind stx with
def expandStrInterpolantChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax :=
chunks.iterateM Syntax.missing fun i elem result => do
- elem ← match elem.isStrInterpolantStrLit? with
+ let elem ← match elem.isStrInterpolantStrLit? with
| none => mkElem elem
| some str => mkElem (mkStxStrLit str);
-- TODO: remove `(` after we write new elabDo
diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean
index 537b0f79ef..e7229ac955 100644
--- a/tests/lean/run/structInst2.lean
+++ b/tests/lean/run/structInst2.lean
@@ -11,7 +11,7 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
@[inline] protected def bind (ma : OptionT2 m α) (f : α → OptionT2 m β) : OptionT2 m β :=
(do {
- a? ← ma;
+ let a? ← ma;
match a? with
| some a => f a
| none => pure none
@@ -21,7 +21,7 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
(HasPure.pure (some a) : m (Option α))
@[inline] protected def orelse (ma : OptionT2 m α) (mb : OptionT2 m α) : OptionT2 m α :=
-(do { a? ← ma;
+(do { let a? ← ma;
match a? with
| some a => pure (some a)
| _ => mb } : m (Option α))
diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
index 97ce2dd9cc..0118f97a5f 100644
--- a/tests/lean/run/structure.lean
+++ b/tests/lean/run/structure.lean
@@ -24,7 +24,7 @@ inductive D
| mk (x y z : Nat) : D
def tst : CoreM Unit :=
-do env ← getEnv;
+do let env ← getEnv;
IO.println (getStructureFields env `Lean.Environment);
check $ getStructureFields env `S4 == #[`toS2, `toS3, `s];
check $ getStructureFields env `S1 == #[`x, `y];
diff --git a/tests/lean/run/stxMacro.lean b/tests/lean/run/stxMacro.lean
index 0474ce332b..bdcc68b4c3 100644
--- a/tests/lean/run/stxMacro.lean
+++ b/tests/lean/run/stxMacro.lean
@@ -7,7 +7,7 @@ syntax "sum! " (many term:max) : term
macro_rules
| `(sum! $x*) => do
- r ← `(0);
+ let r ← `(0);
x.foldlM (fun r elem => `($r + $elem)) r
#check sum! 1 2 3
diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean
index c0a8face9a..64d1adbdd4 100644
--- a/tests/lean/run/synth1.lean
+++ b/tests/lean/run/synth1.lean
@@ -28,34 +28,34 @@ def print {α} [HasToString α] (a : α) : MetaM Unit :=
trace! `Meta.synthInstance (toString a)
-def tst1 : MetaM Unit :=
-do inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
- r ← synthInstance inst;
- print r
+def tst1 : MetaM Unit := do
+let inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
+let r ← synthInstance inst;
+print r
set_option trace.Meta.synthInstance true in
set_option trace.Meta.synthInstance.tryResolve false in
#eval tst1
-def tst2 : MetaM Unit :=
-do inst ← mkAppM `HasBind #[mkConst `IO];
- -- globalInstances ← getGlobalInstances;
- -- print (format globalInstances);
- -- result ← globalInstances.getUnify inst;
- -- print result;
- r ← synthInstance inst;
- print r;
- pure ()
+def tst2 : MetaM Unit := do
+let inst ← mkAppM `HasBind #[mkConst `IO];
+-- globalInstances ← getGlobalInstances;
+-- print (format globalInstances);
+-- result ← globalInstances.getUnify inst;
+-- print result;
+let r ← synthInstance inst;
+print r;
+pure ()
set_option trace.Meta.synthInstance true in
set_option trace.Meta.synthInstance.tryResolve false in
#eval tst2
-def tst3 : MetaM Unit :=
-do inst ← mkAppM `HasBeq #[mkConst `Nat];
- r ← synthInstance inst;
- print r;
- pure ()
+def tst3 : MetaM Unit := do
+let inst ← mkAppM `HasBeq #[mkConst `Nat];
+let r ← synthInstance inst;
+print r;
+pure ()
set_option trace.Meta.synthInstance true in
set_option trace.Meta.synthInstance.tryResolve false in
diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean
index cbeb8e1cd2..a6f06fb602 100644
--- a/tests/lean/run/tactic.lean
+++ b/tests/lean/run/tactic.lean
@@ -9,14 +9,14 @@ axiom simple : forall {p q : Prop}, p → q → p
def print (msg : MessageData) : MetaM Unit :=
trace! `Meta.Tactic msg
-def tst1 : MetaM Unit :=
-do cinfo ← getConstInfo `simple;
- mvar ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
- let mvarId := mvar.mvarId!;
- (_, mvarId) ← introN mvarId 4;
- assumption mvarId;
- result ← instantiateMVars mvar;
- print result
+def tst1 : MetaM Unit := do
+let cinfo ← getConstInfo `simple;
+let mvar ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
+let mvarId := mvar.mvarId!;
+let (_, mvarId) ← introN mvarId 4;
+assumption mvarId;
+let result ← instantiateMVars mvar;
+print result
set_option trace.Meta.Tactic true
diff --git a/tests/lean/run/termElab.lean b/tests/lean/run/termElab.lean
index 34c30fd3d3..885635588e 100644
--- a/tests/lean/run/termElab.lean
+++ b/tests/lean/run/termElab.lean
@@ -6,21 +6,21 @@ open Lean.Elab
open Lean.Elab.Term
def tst1 : TermElabM Unit := do
-opt ← getOptions;
-stx ← `(forall (a b : Nat), Nat);
+let opt ← getOptions;
+let stx ← `(forall (a b : Nat), Nat);
IO.println "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages.
-e ← elabTermAndSynthesize stx none;
+let e ← elabTermAndSynthesize stx none;
logDbgTrace (">>> " ++ e); -- display message when `trace.Elab.debug` is true
IO.println "message 2"
#eval tst1
def tst2 : TermElabM Unit := do
-opt ← getOptions;
+let opt ← getOptions;
let a := mkIdent `a;
let b := mkIdent `b;
-stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
-e ← elabTermAndSynthesize stx none;
+let stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
+let e ← elabTermAndSynthesize stx none;
logDbgTrace (">>> " ++ e);
throwErrorIfErrors
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index f31857c25b..ecc8946ec6 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -3,14 +3,14 @@ new_frontend
open Lean
open Lean.Elab
-def run (input : String) (failIff : Bool := true) : CoreM Unit :=
-do env ← getEnv;
- opts ← getOptions;
- (env, messages) ← liftIO $ process input env opts;
- messages.toList.forM $ fun msg => liftIO (msg.toString >>= IO.println);
- when (failIff && messages.hasErrors) $ throwError "errors have been found";
- when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
- pure ()
+def run (input : String) (failIff : Bool := true) : CoreM Unit := do
+let env ← getEnv;
+let opts ← getOptions;
+let (env, messages) ← liftIO $ process input env opts;
+messages.toList.forM $ fun msg => liftIO (msg.toString >>= IO.println);
+when (failIff && messages.hasErrors) $ throwError "errors have been found";
+when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
+pure ()
open Lean.Parser
diff --git a/tests/lean/run/termparsertest1.lean b/tests/lean/run/termparsertest1.lean
index 8c80fccd09..643cf057b2 100644
--- a/tests/lean/run/termparsertest1.lean
+++ b/tests/lean/run/termparsertest1.lean
@@ -5,8 +5,8 @@ open Lean.Parser
def testParser (input : String) : IO Unit :=
do
-env ← mkEmptyEnvironment;
-stx ← IO.ofExcept $ runParserCategory env `term input "";
+let env ← mkEmptyEnvironment;
+let stx ← IO.ofExcept $ runParserCategory env `term input "";
IO.println stx
def test (is : List String) : IO Unit :=
@@ -16,7 +16,7 @@ is.forM $ fun input => do
def testParserFailure (input : String) : IO Unit :=
do
-env ← mkEmptyEnvironment;
+let env ← mkEmptyEnvironment;
match runParserCategory env `term input "" with
| Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx))
| Except.error msg => IO.println ("failed as expected, error: " ++ msg)
@@ -107,14 +107,14 @@ match x with
"¬ a ∧ b",
"
do
- x ← f a;
- x : Nat ← f a;
+ let x ← f a;
+ let x : Nat ← f a;
g x;
let y := g x;
- (a, b) <- h x y;
+ let (a, b) <- h x y;
let (a, b) := (b, a);
pure (a + b)",
-"do { x ← f a; pure $ a + a }",
+"do { let x ← f a; pure $ a + a }",
"let f : Nat → Nat → Nat
| 0, a => a + 10
| n+1, b => n * b;
diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean
index 2a4e12fa2c..c141b34058 100644
--- a/tests/lean/run/toExpr.lean
+++ b/tests/lean/run/toExpr.lean
@@ -3,7 +3,7 @@ new_frontend
open Lean
unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do
-env ← getEnv;
+let env ← getEnv;
let auxName := `_toExpr._test;
let decl := Declaration.defnDecl {
name := auxName,
diff --git a/tests/lean/run/typeclass_loop.lean b/tests/lean/run/typeclass_loop.lean
index 0bfd17bd77..64faf2edcd 100644
--- a/tests/lean/run/typeclass_loop.lean
+++ b/tests/lean/run/typeclass_loop.lean
@@ -1,5 +1,5 @@
new_frontend
example (M : Type → Type) [Monad M] : ExceptT Unit (ReaderT Unit (StateT Unit M)) Unit := do
-ctx ← read;
+let ctx ← read;
pure ()
diff --git a/tests/lean/run/unexpected_result_with_bind.lean b/tests/lean/run/unexpected_result_with_bind.lean
index 4d454bc6f4..8dccb264d1 100644
--- a/tests/lean/run/unexpected_result_with_bind.lean
+++ b/tests/lean/run/unexpected_result_with_bind.lean
@@ -13,10 +13,10 @@ instance : Monad FooM := {}
def unexpectedBehavior : FooM String := do
let b : Bool := (#[] : Array Nat).isEmpty;
-trueBranch ← pure "trueBranch";
-falseBranch ← pure "falseBranch";
+let trueBranch ← pure "trueBranch";
+let falseBranch ← pure "falseBranch";
(1 : Nat).foldM (λ _ (s : String) => do
- s ← pure $ if b then trueBranch else falseBranch; pure s) ""
+ let s ← pure $ if b then trueBranch else falseBranch; pure s) ""
#eval unexpectedBehavior ()
diff --git a/tests/lean/run/unif_issue.lean b/tests/lean/run/unif_issue.lean
index 6b5f6ea6a8..555c348e5a 100644
--- a/tests/lean/run/unif_issue.lean
+++ b/tests/lean/run/unif_issue.lean
@@ -4,7 +4,7 @@ open Lean
#eval toString $
Unhygienic.run do
- a ← `(Nat.one);
+ let a ← `(Nat.one);
let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing;
let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing;
let discr_2 : _ := a;
@@ -23,7 +23,7 @@ open Lean
#check toString $
Unhygienic.run do
- a ← `(Nat.one);
+ let a ← `(Nat.one);
let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing;
let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing;
let discr_2 : _ := a;
diff --git a/tests/lean/stdio.lean b/tests/lean/stdio.lean
index 9f7ffd743e..5be5c6063e 100644
--- a/tests/lean/stdio.lean
+++ b/tests/lean/stdio.lean
@@ -2,18 +2,18 @@ new_frontend
open IO.FS
def usingIO {α} (x : IO α) := x
#eval usingIO do
-out ← IO.getStdout;
+let out ← IO.getStdout;
(out.putStrLn "print stdout" : IO Unit)
#eval usingIO do
-err ← IO.getStderr;
+let err ← IO.getStderr;
(err.putStr "print stderr" : IO Unit)
open usingIO IO
def test : IO Unit := do
FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do
-{ h₂ ← FS.Handle.mk "stdout2.txt" IO.FS.Mode.write;
+{ let h₂ ← FS.Handle.mk "stdout2.txt" IO.FS.Mode.write;
withStdout (Stream.ofHandle h₁) $ do
println "line 1";
catch