feat: finish commit "using indentation"

src/Lean/Elab/Tactic/Basic.lean

@@ -398,7 +398,7 @@ match g? with
 
 @[builtinTactic «case»] def evalCase : Tactic :=
 fun stx => match_syntax stx with
-  | `(tactic| case $tag $tac) => do
+  | `(tactic| case $tag => $tac:tacticSeq) => do
      let tag := tag.getId;
      gs ← getUnsolvedGoals;
      some g ← findTag? gs tag | throwError "tag not found";

src/Lean/Elab/Tactic/Match.lean

@@ -20,19 +20,19 @@ let matchAlts := matchTac.getArg 4;
 let alts      := (matchAlts.getArg 1).getArgs;
 newAlts ← alts.mapSepElemsM fun alt => do {
   let alt    := alt.updateKind `Lean.Parser.Term.matchAlt;
-  let holeOrTactic := alt.getArg 2;
-  if holeOrTactic.isOfKind `Lean.Parser.Term.syntheticHole then
+  let holeOrTacticSeq := alt.getArg 2;
+  if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
     pure alt
-  else if holeOrTactic.isOfKind `Lean.Parser.Term.hole then do
+  else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then do
     s ← get;
-    let holeName := mkIdentFrom holeOrTactic (parentTag ++ (`match).appendIndexAfter s.nextIdx);
+    let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx);
     newHole ← `(?$holeName:ident);
     modify fun s => { s with nextIdx := s.nextIdx + 1};
     pure $ alt.setArg 2 newHole
   else withFreshMacroScope do
     newHole ← `(?rhs);
     let newHoleId := newHole.getArg 1;
-    newCase ← `(tactic| case $newHoleId $holeOrTactic);
+    newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq );
     modify fun s => { s with cases := s.cases.push newCase };
     pure $ alt.setArg 2 newHole
 };

tests/lean/run/induction1.lean

@@ -19,11 +19,9 @@ by {
 }
 
 theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p :=
-by {
-  induction h using elim2 with
-  | left _  => { apply Or.inr; assumption }
-  | right _ => { apply Or.inl; assumption }
-}
+by induction h using elim2 with
+   | left _  => apply Or.inr; assumption
+   | right _ => apply Or.inl; assumption
 
 theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
@@ -37,16 +35,16 @@ by {
   induction h using elim2 with
   | right h => ?myright
   | left h  => ?myleft;
-  case myleft  { exact Or.inr h };
-  case myright { exact Or.inl h };
+  case myleft  => exact Or.inr h;
+  case myright => exact Or.inl h;
 }
 
 theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
   induction h using elim2 with
   | right h => _
-  | left h  => { refine Or.inr ?_; exact h };
-  case right { exact Or.inl h }
+  | left h  => refine Or.inr ?_; exact h;
+  case right => exact Or.inl h
 }
 
 theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p :=
@@ -71,29 +69,23 @@ by {
 }
 
 theorem tst9 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
-by {
-  cases xs with
-  | nil       => exact rfl
-  | cons z zs => exact absurd rfl (h z zs)
-}
+by cases xs with
+   | nil       => exact rfl
+   | cons z zs => exact absurd rfl (h z zs)
 
 theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q :=
-by {
-  induction h₁ using Iff.elim with
-  | _ h _ => exact h h₂
-}
+by induction h₁ using Iff.elim with
+   | _ h _ => exact h h₂
 
 def Iff2 (m p q : Prop) := p ↔ q
 
 theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q :=
-by {
-  induction h₁ using Iff.elim with
-  | _ h _ => exact h h₂
-}
+by induction h₁ using Iff.elim with
+   | _ h _ => exact h h₂
 
 theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q :=
 by {
-  failIfSuccess (induction h₁ using Iff.elim);
+  failIfSuccess induction h₁ using Iff.elim;
   induction h₂ using Iff.elim with
   | _ h _ => exact h h₃
 }

tests/lean/run/matchtac.lean

@@ -1,20 +1,16 @@
 new_frontend
 
 theorem tst1 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
-by {
-  match h:xs with
-  | []    => exact h₂ h
-  | z::zs => { apply h₁ z zs; assumption }
-}
+by match h:xs with
+   | []    => exact h₂ h
+   | z::zs => apply h₁ z zs; assumption
 
 theorem tst2 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
-by {
-  match h:xs with
-  | []    => ?nilCase
-  | z::zs => ?consCase;
-  case consCase exact h₁ z zs h;
-  case nilCase exact h₂ h;
-}
+by match h:xs with
+   | []    => ?nilCase
+   | z::zs => ?consCase;
+   case consCase => exact h₁ z zs h;
+   case nilCase => exact h₂ h
 
 def tst3 {α β γ : Type} (h : α × β × γ) : β × α × γ :=
 by {
@@ -27,7 +23,7 @@ by {
   match h:xs with
   | []    => _
   | z::zs => _;
-  case match_2 exact h₁ z zs h;
+  case match_2 => exact h₁ z zs h;
   exact h₂ h
 }
 
@@ -37,6 +33,29 @@ by {
   | 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 }
+  case c2 => apply Or.inl; assumption;
+  case c1 => apply Or.inr; apply Or.inl; assumption
 }
+
+theorem tst6 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:=
+by {
+  match h with
+  | Or.inl h          => exact Or.inr (Or.inr h)
+  | Or.inr (Or.inl h) => ?c1
+  | Or.inr (Or.inr h) =>
+    apply Or.inl;
+    assumption;
+  case c1 => apply Or.inr; apply Or.inl; assumption
+}
+
+theorem tst7 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:=
+by match h with
+   | Or.inl h =>
+     exact Or.inr (Or.inr h)
+   | Or.inr (Or.inl h) =>
+     apply Or.inr;
+     apply Or.inl;
+     assumption
+   | Or.inr (Or.inr h) =>
+     apply Or.inl;
+     assumption

tests/lean/run/new_frontend2.lean

@@ -26,8 +26,6 @@ by {
   exact rfl
 }
 
-def ex : {α : _} → {a b c : α} → a = b → b = c → a = c :=
-@by {
-  intro α a b c h₁ h₂;
-  exact Eq.trans h₁ h₂
-}
+def ex : {α : Type} → {a b c : α} → a = b → b = c → a = c :=
+@(by intro α a b c h₁ h₂;
+     exact Eq.trans h₁ h₂)

tests/lean/run/newfrontend1.lean

@@ -103,8 +103,8 @@ theorem simple8 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
   refine! Eq.trans ?pre ?post;
-  case post { exact h1 };
-  case pre { exact h3 };
+  case post => exact h1;
+  case pre => exact h3;
 }
 
 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z :=
@@ -159,7 +159,7 @@ by {
   intros h1 h2 h3;
   traceState;
   apply @Eq.trans;
-  case main.b exact y;
+  case main.b => exact y;
   traceState;
   repeat assumption
 }
@@ -168,7 +168,7 @@ theorem simple14 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intros;
   apply @Eq.trans;
-  case main.b exact y;
+  case main.b => exact y;
   repeat assumption
 }