chore: "begin ... end" ==> "by { ... }"

cc @Kha

tests/lean/run/coroutine.lean

@@ -55,15 +55,15 @@ inductive directSubcoroutine : coroutine α δ β → coroutine α δ β → Pro
 | mk : ∀ (k : α → coroutineResult α δ β) (a : α) (d : δ) (c : coroutine α δ β), k a = yielded d c → directSubcoroutine c (mk k)
 
 theorem directSubcoroutineWf : WellFounded (@directSubcoroutine α δ β) :=
-begin
-  Constructor, intro c,
+by {
+  constructor, intro c,
   apply @coroutine.ind _ _ _
           (fun c => Acc directSubcoroutine c)
           (fun r => ∀ (d : δ) (c : coroutine α δ β), r = yielded d c → Acc directSubcoroutine c),
   { intros k ih, dsimp at ih, Constructor, intros c' h, cases h, apply ih hA hD, assumption },
   { intros, contradiction },
   { intros d c ih d₁ c₁ Heq, injection Heq, subst c, assumption }
-end
+}
 
 /-- Transitive closure of directSubcoroutine. It is not used here, but may be useful when defining
     more complex procedures. -/

tests/lean/run/elab_cmd.lean

@@ -24,7 +24,7 @@ elab "try" t:tactic : tactic => do
   Lean.Elab.Tactic.evalTactic t'
 
 theorem tst (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro h2; intro h3;
   apply @Eq.trans;
   try exact h1; -- `exact h1` fails
@@ -32,4 +32,4 @@ begin
   try exact h3;
   traceState;
   try exact h1;
-end
+}

tests/lean/run/ext_eff.lean

@@ -44,7 +44,7 @@ if h : member.idx eff effs = @member.idx _ u.eff effs u.mem then
 else none
 
 @[inline] def union.decomp (u : union (eff::effs) α) : eff α ⊕ union effs α :=
-begin
+by {
   have prf := @member.prf _ u.eff (eff::effs) u.mem,
   cases h : @member.idx _ u.eff (eff::effs) u.mem,
   case Nat.zero {
@@ -126,11 +126,11 @@ instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) :=
            pure a⟩
 
 @[inline] def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) :=
-eff.handleRelayΣ (fun st a => pure (a, st)) (fun β st x k => begin
+eff.handleRelayΣ (fun st a => pure (a, st)) (fun β st x k => by {
   cases x,
   case State.get { exact k st st },
   case State.put : st' { exact k st' () }
-end) st
+}) st
 
 inductive Exception (ε α : Type) : Type
 | throw {} (ex : ε) : Exception

tests/lean/run/ext_eff_linear.lean

@@ -37,7 +37,7 @@ if h : member.idx eff effs = @member.idx _ u.eff effs u.mem then
 else none
 
 @[inline] def union.decomp (u : union (eff::effs) α) : eff α ⊕ union effs α :=
-begin
+by {
   have prf := @member.prf _ u.eff (eff::effs) u.mem,
   cases h : @member.idx _ u.eff (eff::effs) u.mem,
   case Nat.zero {
@@ -50,7 +50,7 @@ begin
     rw [h] at prf,
     exact Sum.inr { mem := ⟨idx, prf⟩, ..u }
   }
-end
+}
 end
 
 inductive ftcQueue (m : Type → Type 1) : Type → Type → Type 1
@@ -140,11 +140,11 @@ meta instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) :=
            pure a⟩
 
 meta def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) :=
-eff.handleRelayΣ (fun st a => pure (a, st)) (fun β st x k => begin
+eff.handleRelayΣ (fun st a => pure (a, st)) (fun β st x k => by {
   cases x,
   case State.get { exact k st st },
   case State.put : st' { exact k st' () }
-end) st
+}) st
 
 inductive Exception (ε α : Type) : Type
 | throw {} (ex : ε) : Exception

tests/lean/run/extmacro.lean

@@ -7,15 +7,15 @@ syntax "trivial" : tactic
 ext_tactic trivial => apply Eq.refl
 
 theorem tst1 (x : Nat) : x = x :=
-begin trivial end
+by trivial
 
 -- theorem tst2 (x y : Nat) (h : x = y) : x = y :=
--- begin trivial end -- fail as expected
+-- by trivial -- fail as expected
 
 ext_tactic trivial => assumption
 
 theorem tst1b (x : Nat) : x = x :=
-begin trivial end -- still works
+by trivial -- still works
 
 theorem tst2 (x y : Nat) (h : x = y) : x = y :=
-begin trivial end -- works too
+by trivial -- works too

tests/lean/run/generalize.lean

@@ -1,35 +1,35 @@
 new_frontend
 
 theorem tst0 (x : Nat) : x + 0 = x + 0 :=
-begin
+by {
   generalize x + 0 = y;
   exact (Eq.refl y)
-end
+}
 
 theorem tst1 (x : Nat) : x + 0 = x + 0 :=
-begin
+by {
   generalize h : x + 0 = y;
   exact (Eq.refl y)
-end
+}
 
 theorem tst2 (x y w : Nat) (h : y = w) : (x + x) + w  = (x + x) + y :=
-begin
+by {
   generalize h' : x + x = z;
   subst y;
   exact Eq.refl $ z + w
-end
+}
 
 theorem tst3 (x y w : Nat) (h : x + x = y) : (x + x) + (x+x)  = (x + x) + y :=
-begin
+by {
   generalize h' : x + x = z;
   subst z;
   subst y;
   exact rfl
-end
+}
 
 theorem tst4 (x y w : Nat) (h : y = w) : (x + x) + w  = (x + x) + y :=
-begin
+by {
   generalize h' : x + y = z; -- just add equality
   subst h;
   exact rfl
-end
+}

tests/lean/run/induction1.lean

@@ -5,95 +5,95 @@ Or.elim major left right
 new_frontend
 
 theorem tst0 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   induction h;
   { apply Or.inr; assumption };
   { apply Or.inl; assumption }
-end
+}
 
 theorem tst1 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   induction h with
   | inr h2 => exact Or.inl h2
   | inl h1 => exact Or.inr h1
-end
+}
 
 theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   induction h using elim2 with
   | left _  => { apply Or.inr; assumption }
   | right _ => { apply Or.inl; assumption }
-end
+}
 
 theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   induction h using elim2 with
   | right h => exact Or.inl h
   | left h  => exact Or.inr h
-end
+}
 
 theorem tst4 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   induction h using elim2 with
   | right h => ?myright
   | left h  => ?myleft;
   case myleft  { exact Or.inr h };
   case myright { exact Or.inl h };
-end
+}
 
 theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   induction h using elim2 with
   | right h => _
   | left h  => { refine Or.inr _; exact h };
   case right { exact Or.inl h }
-end
+}
 
 theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-begin
+by {
   cases h with
   | inr h2 => exact Or.inl h2
   | inl h1 => exact Or.inr h1
-end
+}
 
 theorem tst7 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
-begin
+by {
   induction xs with
   | nil          => exact rfl
   | cons z zs ih => exact absurd rfl (h z zs)
-end
+}
 
 theorem tst8 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
-begin
+by {
   induction xs;
   exact rfl;
   exact absurd rfl $ h _ _
-end
+}
 
 theorem tst9 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
-begin
+by {
   cases xs with
   | nil       => exact rfl
   | cons z zs => exact absurd rfl (h z zs)
-end
+}
 
 theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q :=
-begin
+by {
   induction h₁ using Iff.elim with
   | _ h _ => exact h h₂
-end
+}
 
 def Iff2 (m p q : Prop) := p ↔ q
 
 theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q :=
-begin
+by {
   induction h₁ using Iff.elim with
   | _ h _ => exact h h₂
-end
+}
 
 theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q :=
-begin
+by {
   failIfSuccess (induction h₁ using Iff.elim);
   induction h₂ using Iff.elim with
   | _ h _ => exact h h₃
-end
+}

tests/lean/run/inj1.lean

@@ -1,44 +1,44 @@
 new_frontend
 
 theorem test1 {α} (a b : α) (as bs : List α) (h : a::as = b::bs) : a = b :=
-begin
+by {
   injection h;
   assumption;
-end
+}
 
 theorem test2 {α} (a b : α) (as bs : List α) (h : a::as = b::bs) : a = b :=
-begin
+by {
   injection h with h1 h2;
   exact h1
-end
+}
 
 theorem test3 {α} (a b : α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : as = bs :=
 have a::as = b::bs from h (a::as) (b::bs);
-begin
+by {
   injection this with h1 h2;
   exact h2
-end
+}
 
 theorem test4 {α} (a b : α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : as = bs :=
-begin
+by {
   injection h (a::as) (b::bs) with h1 h2;
   exact h2
-end
+}
 
 theorem test5 {α} (a : α) (as : List α) (h : a::as = []) : 0 > 1 :=
-begin
+by {
   injection h
-end
+}
 
 theorem test6 (n : Nat) (h : n+1 = 0) : 0 > 1 :=
-begin
+by {
   injection h
-end
+}
 
 theorem test7 (n m k : Nat) (h : n + 1 = m + 1) : m = k → n = k :=
-begin
+by {
   injection h with h₁;
   subst h₁;
   intro h₂;
   exact h₂
-end
+}

tests/lean/run/inj2.lean

@@ -11,36 +11,30 @@ inductive Fin2 : Nat → Type
 new_frontend
 
 theorem test1 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : a₁ = a₂ :=
-begin
+by {
   injection h;
   assumption
-end
+}
 
 theorem test2 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : v = w :=
-begin
+by {
   injection h with h1 h2 h3 h4;
   assumption
-end
+}
 
 theorem test3 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : v = w :=
-begin
+by {
   injection h with _ _ _ h4;
   exact h4
-end
+}
 
 theorem test4 {α} (v : Fin2 0) : α :=
-begin
-  cases v
-end
+by cases v
 
 def test5 {α β} {n} (v : Vec2 α β (n+1)) : α :=
-begin
-  cases v with
-  | cons h1 h2 n tail => exact h1
-end
+by cases v with
+   | cons h1 h2 n tail => exact h1
 
 def test6 {α β} {n} (v : Vec2 α β (n+2)) : α :=
-begin
-  cases v with
-  | cons h1 h2 n tail => exact h1
-end
+by cases v with
+   | cons h1 h2 n tail => exact h1

tests/lean/run/intromacro.lean

@@ -4,20 +4,20 @@ structure S :=
 (x y z : Nat := 0)
 
 def f1 : Nat × Nat → S → Nat :=
-begin
+by {
   intro (x, y);
   intro ⟨a, b, c⟩;
   exact x+y+a
-end
+}
 
 theorem ex1 : f1 (10, 20) { x := 10 } = 40 :=
 rfl
 
 def f2 : Nat × Nat → S → Nat :=
-begin
+by {
   intro (a, b) { y := y, .. };
   exact a+b+y
-end
+}
 
 #eval f2 (10, 20) { y := 5 }
 
@@ -25,10 +25,10 @@ theorem ex2 : f2 (10, 20) { y := 5 } = 35 :=
 rfl
 
 def f3 : Nat × Nat → S → S → Nat :=
-begin
+by {
   intro (a, b) { y := y, .. } s;
   exact a+b+y+s.x
-end
+}
 
 #eval f3 (10, 20) { y := 5 } { x := 1 }
 

tests/lean/run/matchtac.lean

@@ -1,42 +1,42 @@
 new_frontend
 
 theorem tst1 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
-begin
+by {
   match h:xs with
   | []    => exact h₂ h
   | z::zs => { apply h₁ z zs; assumption }
-end
+}
 
 theorem tst2 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
-begin
+by {
   match h:xs with
   | []    => ?nilCase
   | z::zs => ?consCase;
   case consCase exact h₁ z zs h;
   case nilCase exact h₂ h;
-end
+}
 
 def tst3 {α β γ : Type} (h : α × β × γ) : β × α × γ :=
-begin
+by {
   match h with
   | (a, b, c) => exact (b, a, c)
-end
+}
 
 theorem tst4 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
-begin
+by {
   match h:xs with
   | []    => _
   | z::zs => _;
   case match_2 exact h₁ z zs h;
   exact h₂ h
-end
+}
 
 theorem tst5 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:=
-begin
+by {
   match h with
   | Or.inl h          => exact Or.inr (Or.inr h)
   | Or.inr (Or.inl h) => ?c1
   | Or.inr (Or.inr h) => ?c2;
   case c2 { apply Or.inl; assumption };
   { apply Or.inr; apply Or.inl; assumption }
-end
+}

tests/lean/run/newfrontend1.lean

@@ -42,15 +42,15 @@ def apply := "hello"
 #check apply
 
 theorem simple1 (x y : Nat) (h : x = y) : x = y :=
-begin
+by {
   assumption
-end
+}
 
 theorem simple2 (x y : Nat) : x = y → x = y :=
-begin
+by {
   intro h;
   assumption
-end
+}
 
 syntax "intro2" : tactic
 
@@ -58,10 +58,10 @@ macro_rules
 | `(tactic| intro2) => `(tactic| intro; intro )
 
 theorem simple3 (x y : Nat) : x = x → x = y → x = y :=
-begin
+by {
   intro2;
   assumption
-end
+}
 
 macro intro3 : tactic => `(intro; intro; intro)
 macro check2 x:term : command => `(#check $x #check $x)
@@ -73,71 +73,71 @@ check2 0+1
 check2 foo 0,1
 
 theorem simple4 (x y : Nat) : y = y → x = x → x = y → x = y :=
-begin
+by {
   intro3;
   assumption
-end
+}
 
 theorem simple5 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro _; intro h3;
   exact Eq.trans h3 h1
-end
+}
 
 theorem simple6 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro _; intro h3;
   refine Eq.trans _ h1;
   assumption
-end
+}
 
 theorem simple7 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro _; intro h3;
   refine Eq.trans ?pre ?post;
   exact y;
   { exact h3 };
   { exact h1 }
-end
+}
 
 theorem simple8 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro _; intro h3;
   refine Eq.trans ?pre ?post;
   case post { exact h1 };
   case pre { exact h3 };
-end
+}
 
 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 _ h3;
   traceState;
   { refine Eq.trans ?pre ?post;
     (exact h1) <|> (exact y; exact h3; assumption) }
-end
+}
 
 namespace Foo
   def Prod.mk := 1
   #check (⟨2, 3⟩ : Prod _ _)
-end Foo
+} Foo
 
 theorem simple10 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro h2; intro h3;
   skip;
   apply Eq.trans;
   exact h3;
   assumption
-end
+}
 
 theorem simple11 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro h2; intro h3;
   apply @Eq.trans;
   traceState;
   exact h3;
   assumption
-end
+}
 
 macro try t:tactic : tactic => `($t <|> skip)
 
@@ -147,7 +147,7 @@ macro_rules
 
 
 theorem simple12 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intro h1; intro h2; intro h3;
   apply @Eq.trans;
   try exact h1; -- `exact h1` fails
@@ -155,38 +155,38 @@ begin
   try exact h3;
   traceState;
   try exact h1;
-end
+}
 
 theorem simple13 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 h2 h3;
   traceState;
   apply @Eq.trans;
   case main.b exact y;
   traceState;
   repeat assumption
-end
+}
 
 theorem simple14 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros;
   apply @Eq.trans;
   case main.b exact y;
   repeat assumption
-end
+}
 
 theorem simple15 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 h2 h3;
   revert y;
   intros y h1 h3;
   apply Eq.trans;
   exact h3;
   exact h1
-end
+}
 
 theorem simple16 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 h2 h3;
   try (clear x); -- should fail
   clear h2;
@@ -194,7 +194,7 @@ begin
   apply Eq.trans;
   exact h3;
   exact h1
-end
+}
 
 macro "blabla" : tactic => `(assumption)
 
@@ -204,7 +204,7 @@ def blabla := 100
 #check blabla
 
 theorem simple17 (x : Nat) (h : x = 0) : x = 0 :=
-begin blabla end
+by blabla
 
 theorem simple18 (x : Nat) (h : x = 0) : x = 0 :=
 by blabla

tests/lean/run/newfrontend3.lean

@@ -10,7 +10,7 @@ def tst : Nat :=
 f (fun n => (fun x => x, true))
 
 theorem ex : id (Nat → Nat) :=
-begin
+by {
   intro;
   assumption
-end
+}

tests/lean/run/obtain.lean

@@ -15,11 +15,11 @@ macro "obtain " p:term " from " d:term "; " body:tactic : tactic =>
 `(tactic| match $d:term with | $p:term => _; $body)
 
 theorem tst3 {p q r} (h : p ∧ q ∧ r) : q ∧ p ∧ r :=
-begin
+by {
   obtain ⟨h₁, ⟨h₂, h₃⟩⟩ from h;
   apply And.intro;
   assumption;
   apply And.intro;
   assumption;
   assumption
-end
+}

tests/lean/run/revert1.lean

@@ -1,17 +1,17 @@
 new_frontend
 
 theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 h2 h3;
   revert h2;
   intro h2;
   exact Eq.trans h3 h1
-end
+}
 
 theorem tst2 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 h2 h3;
   revert y;
   intros y hb ha;
   exact Eq.trans ha hb
-end
+}

tests/lean/run/subst1.lean

@@ -3,30 +3,30 @@ new_frontend
 set_option trace.Meta.Tactic.subst true
 
 theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-begin
+by {
   intros h1 h2 h3;
   subst x;
   assumption
-end
+}
 
 theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z :=
-begin
+by {
   intros h1 h2;
   subst h1;
   subst h2;
   exact rfl
-end
+}
 
 def BV (n : Nat) : Type := Unit
 
 theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1) w :=
-begin
+by {
   subst h1;
   apply h2
-end
+}
 
 theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w :=
-begin
+by {
   subst n;
   apply h2
-end
+}

tests/lean/run/tactic1.lean

@@ -1,46 +1,46 @@
 new_frontend
 
 theorem ex1 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
-begin
+by {
   clear y x;
   exact z
-end
+}
 
 theorem ex2 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
-begin
+by {
   clear x y;
   exact z
-end
+}
 
 theorem ex3 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
-begin
+by {
   have y = z from h₂.symm;
   apply Eq.trans;
   exact h₁;
   assumption
-end
+}
 
 theorem ex4 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
-begin
+by {
   let h₃ : y = z := h₂.symm;
   apply Eq.trans;
   exact h₁;
   exact h₃
-end
+}
 
 theorem ex5 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
-begin
+by {
   let! h₃ : y = z := h₂.symm;
   apply Eq.trans;
   exact h₁;
   exact h₃
-end
+}
 
 theorem ex6 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : id (x + 0 = z) :=
-begin
+by {
   show x = z;
   let! h₃ : y = z := h₂.symm;
   apply Eq.trans;
   exact h₁;
   exact h₃
-end
+}

tests/lean/run/tacticExtOverlap.lean

@@ -8,20 +8,20 @@ macro_rules [myintro]
 | `(tactic| intros $x*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom {} "intros", mkNullNode x.getSepElems]
 
 theorem tst1 {p q : Prop} : p → q → p :=
-begin
+by {
   intros h1, h2;
   assumption
-end
+}
 
 theorem tst2 {p q : Prop} : p → q → p :=
-begin
+by {
   intros h1; -- the builtin and myintro overlap here.
   intros h2; -- the builtin and myintro overlap here.
   assumption
-end
+}
 
 theorem tst3 {p q : Prop} : p → q → p :=
-begin
+by {
   intros h1 h2;
   assumption
-end
+}