From 3bff6d3843d7c31700a922d5b3b454786152430f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 27 Oct 2024 18:04:51 -0700 Subject: [PATCH] fixed formatter issue --- .../PrettyPrinter/Delaborator/Builtins.lean | 4 +- src/Lean/PrettyPrinter/Formatter.lean | 65 +++++++++++-------- src/lake/Lake/Toml/ParserUtil.lean | 2 +- tests/lean/run/2846.lean | 14 +++- tests/lean/run/4320.lean | 2 +- tests/lean/run/5424.lean | 10 +++ tests/lean/run/974.lean | 9 ++- tests/lean/run/eqnsPrio.lean | 6 +- tests/lean/run/funind_demo.lean | 4 +- tests/lean/run/funind_fewer_levels.lean | 6 +- tests/lean/run/funind_proof.lean | 2 +- tests/lean/run/funind_structural.lean | 12 ++-- tests/lean/run/funind_structural_mutual.lean | 2 +- tests/lean/run/funind_tests.lean | 58 ++++++++--------- tests/lean/run/namePatEqThm.lean | 5 +- tests/lean/run/reserved.lean | 12 ++-- tests/lean/run/structuralMutual.lean | 10 +-- tests/lean/run/unfoldLemma.lean | 6 +- tests/lean/run/wfEqns5.lean | 24 +++---- 19 files changed, 143 insertions(+), 110 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 0a39b839185c..047662ecbabb 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -898,7 +898,7 @@ Similar to `delabBinders`, but tracking whether `forallE` is dependent or not. See issue #1571 -/ private partial def delabForallBinders (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do - let dep := !(← getExpr).isArrow + let dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false if !curNames.isEmpty && dep != curDep then -- don't group delabGroup curNames curDep (← delab) @@ -926,7 +926,7 @@ def delabForall : Delab := do | BinderInfo.instImplicit => `(bracketedBinderF|[$curNames.back : $stxT]) | _ => -- NOTE: non-dependent arrows are available only for the default binder info - if dependent || (← getOptionsAtCurrPos).get ppPiBinderNames false then + if dependent then if prop && !(← getPPOption getPPPiBinderTypes) then return ← `(∀ $curNames:ident*, $stxBody) else diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 8b9324fe3d42..23f7ec304232 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -30,16 +30,18 @@ structure Context where structure State where stxTrav : Syntax.Traverser - -- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual - -- content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly. + /-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual + content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly. -/ leadWord : String := "" - -- Whether the generated format begins with the result of an ungrouped category formatter. + /-- When the `leadWord` is nonempty, whether it is an identifier. Identifiers get space inserted between them. -/ + leadWordIdent : Bool := false + /-- Whether the generated format begins with the result of an ungrouped category formatter. -/ isUngrouped : Bool := false - -- Whether the resulting format must be grouped when used in a category formatter. - -- If the flag is set to false, then categoryParser omits the fill+nest operation. + /-- Whether the resulting format must be grouped when used in a category formatter. + If the flag is set to false, then categoryParser omits the fill+nest operation. -/ mustBeGrouped : Bool := true - -- Stack of generated Format objects, analogous to the Syntax stack in the parser. - -- Note, however, that the stack is reversed because of the right-to-left traversal. + /-- Stack of generated Format objects, analogous to the Syntax stack in the parser. + Note, however, that the stack is reversed because of the right-to-left traversal. -/ stack : Array Format := #[] end Formatter @@ -121,7 +123,7 @@ private def push (f : Format) : FormatterM Unit := def pushWhitespace (f : Format) : FormatterM Unit := do push f - modify fun st => { st with leadWord := "", isUngrouped := false } + modify fun st => { st with leadWord := "", leadWordIdent := false, isUngrouped := false } def pushLine : FormatterM Unit := pushWhitespace Format.line @@ -335,7 +337,7 @@ def parseToken (s : String) : FormatterM ParserState := options := ← getOptions } ((← read).table) (Parser.mkParserState s) -def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do +def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit := do match info with | SourceInfo.original _ _ ss _ => -- preserve non-whitespace content (i.e. comments) @@ -346,23 +348,34 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do push s!"\n{ss'}" else push s!" {ss'}" - modify fun st => { st with leadWord := "" } + modify fun st => { st with leadWord := "", leadWordIdent := false } | _ => pure () let st ← get - -- If there is no space between `tk` and the next word, see if we would parse more than `tk` as a single token + -- If there is no space between `tk` and the next word, see if we should insert a discretionary space. if st.leadWord != "" && tk.trimRight == tk then - let tk' := tk.trimLeft - let t ← parseToken $ tk' ++ st.leadWord - if t.pos <= tk'.endPos then - -- stopped within `tk` => use it as is, extend `leadWord` if not prefixed by whitespace + let insertSpace ← do + if ident && st.leadWordIdent then + -- Both idents => need space + pure true + else + -- Check if we would parse more than `tk` as a single token + let tk' := tk.trimLeft + let t ← parseToken $ tk' ++ st.leadWord + if t.pos ≤ tk'.endPos then + -- stopped within `tk` => use it as is + pure false + else + -- stopped after `tk` => add space + pure true + if !insertSpace then + -- extend `leadWord` if not prefixed by whitespace push tk - modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" } + modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "", leadWordIdent := ident } else - -- stopped after `tk` => add space pushLine push tk - modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" } + modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident } else -- already separated => use `tk` as is if st.leadWord == "" then @@ -372,7 +385,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do push tk.trimRight else push tk -- preserve special whitespace for tokens like ":=\n" - modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" } + modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident } match info with | SourceInfo.original ss _ _ _ => @@ -395,7 +408,7 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do let stx ← getCur if stx.isToken sym then do let (Syntax.atom info _) ← pure stx | unreachable! - withMaybeTag (getExprPos? stx) (pushToken info sym) + withMaybeTag (getExprPos? stx) (pushToken info sym false) goLeft else do trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected symbol '{sym}'" @@ -410,9 +423,9 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do let Syntax.atom info val ← getCur | throwError m!"not an atom: {← getCur}" if val == sym.trim then - pushToken info sym + pushToken info sym false else - pushToken info asciiSym; + pushToken info asciiSym false goLeft @[combinator_formatter identNoAntiquot] @@ -423,14 +436,14 @@ def identNoAntiquot.formatter : Formatter := do let id := id.simpMacroScopes let table := (← read).table let isToken (s : String) : Bool := (table.find? s).isSome - withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken))) + withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)) true) goLeft @[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do checkKind identKind let Syntax.ident info _ id _ ← getCur | throwError m!"not an ident: {← getCur}" - pushToken info id.toString + pushToken info id.toString true goLeft @[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter @@ -441,7 +454,7 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do checkKind k let Syntax.atom info val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx) | throwError m!"not an atom: {stx}" - pushToken info val + pushToken info val false goLeft @[combinator_formatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind @@ -490,7 +503,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do @[combinator_formatter checkStackTop] def checkStackTop.formatter : Formatter := pure () @[combinator_formatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := -- prevent automatic whitespace insertion - modify fun st => { st with leadWord := "" } + modify fun st => { st with leadWord := "", leadWordIdent := false } @[combinator_formatter checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure () @[combinator_formatter checkTailWs] def checkTailWs.formatter : Formatter := pure () @[combinator_formatter checkColEq] def checkColEq.formatter : Formatter := pure () diff --git a/src/lake/Lake/Toml/ParserUtil.lean b/src/lake/Lake/Toml/ParserUtil.lean index 43e3d2070ea1..de874dc03549 100644 --- a/src/lake/Lake/Toml/ParserUtil.lean +++ b/src/lake/Lake/Toml/ParserUtil.lean @@ -161,7 +161,7 @@ open Formatter Syntax.MonadTraverser in let .atom info val := stx | trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected atom" throwBacktrack - withMaybeTag (getSyntaxExprPos? stx) (pushToken info val) + withMaybeTag (getSyntaxExprPos? stx) (pushToken info val false) goLeft @[combinator_parenthesizer atom] diff --git a/tests/lean/run/2846.lean b/tests/lean/run/2846.lean index aabdbc357c48..44ca7773c033 100644 --- a/tests/lean/run/2846.lean +++ b/tests/lean/run/2846.lean @@ -48,13 +48,23 @@ def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0 /-! Named argument after inaccessible name, still stays after the colon. -But, it does not print using named pi notation since this is not a dependent type. +Prints with named pi notation. -/ def foo'' : String → (needle : String) → String := fun _ yo => yo -/-- info: foo'' : (a✝needle : String) → String -/ +/-- info: foo'' : String → (needle : String) → String -/ #guard_msgs in #check foo'' +/-! +Named argument after inaccessible name that's still a dependent argument. +Stays after the colon, and the names are grouped. +-/ + +def foo''' : (_ : Nat) → (n : Nat) → Fin (n + by clear n; assumption) := sorry + +/-- info: foo''' : (x✝ n : Nat) → Fin (n + x✝) -/ +#guard_msgs in #check foo''' + /-! Named argument after inaccessible name, still stays after the colon. Here, because it's a dependent type the named pi notation shows the name. diff --git a/tests/lean/run/4320.lean b/tests/lean/run/4320.lean index b524a9fb0b59..c60bb3afc478 100644 --- a/tests/lean/run/4320.lean +++ b/tests/lean/run/4320.lean @@ -8,7 +8,7 @@ def many_map {α β : Type} (f : α → β) : Many α → Many β /-- info: many_map.induct {α β : Type} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none) - (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a : Many α), motive a + (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a✝ : Many α), motive a✝ -/ #guard_msgs in #check many_map.induct diff --git a/tests/lean/run/5424.lean b/tests/lean/run/5424.lean index 92a64df01b02..cf38cb783381 100644 --- a/tests/lean/run/5424.lean +++ b/tests/lean/run/5424.lean @@ -1,3 +1,4 @@ +import Lean /-! # Long runs of identifiers should include line breaks -/ @@ -19,3 +20,12 @@ info: foo Nat -/ #guard_msgs(whitespace := exact) in #check foo + +/-! +Issue pointed out by Mario: need spaces between `x✝` and `y✝`. +-/ +/-- +info: def foo✝ (x✝ y✝ : Nat✝) := + x✝ +-/ +#guard_msgs in #eval do Lean.PrettyPrinter.ppCommand (← `(command| def foo (x y : Nat) := x)) diff --git a/tests/lean/run/974.lean b/tests/lean/run/974.lean index 395d1918c23a..0953edb43f36 100644 --- a/tests/lean/run/974.lean +++ b/tests/lean/run/974.lean @@ -12,23 +12,22 @@ attribute [simp] Formula.count_quantifiers /-- info: Formula.count_quantifiers.eq_1.{u_1} : - ∀ (x : Nat) (f₁ f₂ : Formula x), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers + ∀ (x✝ : Nat) (f₁ f₂ : Formula x✝), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers -/ #guard_msgs in #check Formula.count_quantifiers.eq_1 /-- info: Formula.count_quantifiers.eq_2.{u_1} : - ∀ (x : Nat) (f : Formula (x + 1)), f.all.count_quantifiers = f.count_quantifiers + 1 + ∀ (x✝ : Nat) (f : Formula (x✝ + 1)), f.all.count_quantifiers = f.count_quantifiers + 1 -/ #guard_msgs in #check Formula.count_quantifiers.eq_2 /-- info: Formula.count_quantifiers.eq_3.{u_1} : - ∀ (x : Nat) (x_1 : Formula x), - (∀ (f₁ f₂ : Formula x), x_1 = f₁.imp f₂ → False) → - (∀ (f : Formula (x + 1)), x_1 = f.all → False) → x_1.count_quantifiers = 0 + ∀ (x✝ : Nat) (x✝¹ : Formula x✝) (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = f₁.imp f₂ → False) + (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = f.all → False), x✝¹.count_quantifiers = 0 -/ #guard_msgs in #check Formula.count_quantifiers.eq_3 diff --git a/tests/lean/run/eqnsPrio.lean b/tests/lean/run/eqnsPrio.lean index 97613ad6e865..0937b67f5a32 100644 --- a/tests/lean/run/eqnsPrio.lean +++ b/tests/lean/run/eqnsPrio.lean @@ -11,13 +11,15 @@ def foo : Bool → Nat → Nat | _, n+1 => foo .false n termination_by _ n => n -/-- info: foo.eq_1 : ∀ (x : Bool), foo x 0 = 0 -/ +/-- info: foo.eq_1 : ∀ (x✝ : Bool), foo x✝ 0 = 0 -/ #guard_msgs in #check foo.eq_1 /-- info: foo.eq_2 (n : Nat) : foo true n.succ = foo true n -/ #guard_msgs in #check foo.eq_2 -/-- info: foo.eq_3 : ∀ (x : Bool) (n : Nat), (x = true → False) → foo x n.succ = foo false n -/ +/-- +info: foo.eq_3 : ∀ (x✝ : Bool) (n : Nat) (x_3 : x✝ = true → False), foo x✝ n.succ = foo false n +-/ #guard_msgs in #check foo.eq_3 diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean index f27d0d4808b1..fb5b635b7d28 100644 --- a/tests/lean/run/funind_demo.lean +++ b/tests/lean/run/funind_demo.lean @@ -9,7 +9,7 @@ def ackermann : Nat → Nat → Nat info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0) (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) : - ∀ (a a_1 : Nat), motive a a_1 + ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹ -/ #guard_msgs in #check ackermann.induct @@ -19,7 +19,7 @@ def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ /-- info: Tree.rev.induct (motive : Tree → Prop) - (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a + (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a✝ : Tree), motive a✝ -/ #guard_msgs in #check Tree.rev.induct diff --git a/tests/lean/run/funind_fewer_levels.lean b/tests/lean/run/funind_fewer_levels.lean index 519b4e44bf32..dc26e889ac0d 100644 --- a/tests/lean/run/funind_fewer_levels.lean +++ b/tests/lean/run/funind_fewer_levels.lean @@ -11,7 +11,7 @@ def foo.{u} : Nat → PUnit.{u} /-- info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check foo.induct @@ -31,7 +31,7 @@ termination_by xs => xs /-- info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive []) - (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a + (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a✝ : List α), motive a✝ -/ #guard_msgs in #check foo.induct @@ -58,7 +58,7 @@ end /-- info: Mutual.foo.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) - (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a + (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a✝ : Nat), motive1 a✝ -/ #guard_msgs in #check foo.induct diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean index bff44bf0e49b..aaf449b03180 100644 --- a/tests/lean/run/funind_proof.lean +++ b/tests/lean/run/funind_proof.lean @@ -35,7 +35,7 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2 (case1 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1)) (case2 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1)) (case3 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) (case4 : motive2 []) - (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a + (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a✝ : Term), motive1 a✝ -/ #guard_msgs in #check replaceConst.induct diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean index 20b6ce5f565a..731e202e7611 100644 --- a/tests/lean/run/funind_structural.lean +++ b/tests/lean/run/funind_structural.lean @@ -11,7 +11,7 @@ termination_by structural x => x /-- info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) - (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check fib.induct @@ -25,7 +25,7 @@ termination_by structural x => x /-- info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc) (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) : - ∀ (a a_1 : Nat), motive a a_1 + ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹ -/ #guard_msgs in #check binary.induct @@ -41,7 +41,7 @@ termination_by structural _ x => x info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0) (case2 : ∀ (acc : Bool), motive acc 1) (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ) : - ∀ (a : Bool) (a_1 : Nat), motive a a_1 + ∀ (a✝ : Bool) (a✝¹ : Nat), motive a✝ a✝¹ -/ #guard_msgs in #check binary'.induct @@ -56,7 +56,7 @@ termination_by structural x => x info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop) (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t []) (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) : - ∀ (a : List α) (a_1 : List β), motive a a_1 + ∀ (a✝ : List α) (a✝¹ : List β), motive a✝ a✝¹ -/ #guard_msgs in #check zip.induct @@ -94,7 +94,7 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1) (case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero) (case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool) - {n : Nat} (m : Nat) : ∀ (a f : Finn n), motive x m a f + {n : Nat} (m : Nat) : ∀ (a✝ f : Finn n), motive x m a✝ f -/ #guard_msgs in #check Finn.min.induct @@ -195,7 +195,7 @@ info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → (case6 : ∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a), motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env) - {ctx : List Ty} {ty : Ty} : ∀ (a : Term ctx ty) (a_1 : HList Ty.denote ctx), motive a a_1 + {ctx : List Ty} {ty : Ty} : ∀ (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx), motive a✝ a✝¹ -/ #guard_msgs in #check TermDenote.Term.denote.induct diff --git a/tests/lean/run/funind_structural_mutual.lean b/tests/lean/run/funind_structural_mutual.lean index 399764103c81..662039d15316 100644 --- a/tests/lean/run/funind_structural_mutual.lean +++ b/tests/lean/run/funind_structural_mutual.lean @@ -26,7 +26,7 @@ info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (moti (case1 : ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf)) (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) : - ∀ (a : Tree α), motive_1 a + ∀ (a✝ : Tree α), motive_1 a✝ -/ #guard_msgs in #check Tree.size.induct diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 503052b211d0..f64093b37d11 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -16,7 +16,7 @@ termination_by p => p info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m)) (case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0)) (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ)) : - ∀ (a : Nat × Nat), motive a + ∀ (a✝ : Nat × Nat), motive a✝ -/ #guard_msgs in #check ackermann.induct @@ -35,7 +35,7 @@ termination_by n m => (n, m) info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0) (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) : - ∀ (a a_1 : Nat), motive a a_1 + ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹ -/ #guard_msgs in #check ackermann.induct @@ -50,7 +50,7 @@ def Tree.rev : Tree → Tree /-- info: Tree.rev.induct (motive : Tree → Prop) - (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a + (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a✝ : Tree), motive a✝ -/ #guard_msgs in #check Tree.rev.induct @@ -64,7 +64,7 @@ termination_by n => n /-- info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) - (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check fib.induct @@ -79,7 +79,7 @@ termination_by n => n /-- info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) - (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ) : ∀ (a : Nat), motive a + (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check have_tailrec.induct @@ -95,7 +95,7 @@ termination_by n => n /-- info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check have_non_tailrec.induct @@ -110,7 +110,7 @@ termination_by n => n /-- info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check let_tailrec.induct @@ -126,7 +126,7 @@ termination_by n => n /-- info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check let_non_tailrec.induct @@ -145,7 +145,7 @@ termination_by n => n /-- info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ) - (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_ite_tailrec.induct @@ -165,7 +165,7 @@ termination_by n => n /-- info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) - (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_ite_non_tailrec.induct @@ -212,7 +212,7 @@ termination_by n => n /-- info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0)) - (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_match_refining_tailrec.induct @@ -228,7 +228,7 @@ termination_by i /-- info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0) (case2 : ∀ (n : Nat), motive 0 n.succ) (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i n.succ) - (i : Nat) : ∀ (a : Nat), motive i a + (i : Nat) : ∀ (a✝ : Nat), motive i a✝ -/ #guard_msgs in #check with_arg_refining_match1.induct @@ -260,7 +260,7 @@ termination_by n => n /-- info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ) - (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_other_match_tailrec.induct @@ -275,7 +275,7 @@ termination_by n => n /-- info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1) (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) : - ∀ (a a_1 a_2 a_3 : Nat), motive a a_1 a_2 a_3 + ∀ (a✝ a✝¹ a✝² a✝³ : Nat), motive a✝ a✝¹ a✝² a✝³ -/ #guard_msgs in #check with_mixed_match_tailrec.induct @@ -294,7 +294,7 @@ termination_by n => n info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive n.succ 0 x a a_1) (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1) : - ∀ (a a_1 a_2 a_3 a_4 : Nat), motive a a_1 a_2 a_3 a_4 + ∀ (a✝ a✝¹ a✝² a✝³ a✝⁴ : Nat), motive a✝ a✝¹ a✝² a✝³ a✝⁴ -/ #guard_msgs in #check with_mixed_match_tailrec2.induct @@ -311,7 +311,7 @@ termination_by n => n /-- info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_match_non_tailrec.induct @@ -334,7 +334,7 @@ info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : mo | 0 => motive 0 | m => motive m) → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_match_non_tailrec_refining.induct @@ -351,7 +351,7 @@ termination_by n => n /-- info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3) (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) : - ∀ (a : Nat), motive a + ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check with_overlap.induct @@ -368,7 +368,7 @@ termination_by n => n /-- info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0) - (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a : Nat), motive a + (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check unary.induct @@ -380,7 +380,7 @@ termination_by n => n /-- info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) - (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) : ∀ (a a_1 : Nat), motive a a_1 + (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) : ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹ -/ #guard_msgs in #check binary.induct @@ -512,7 +512,7 @@ def foo {α} (x : α) : List α → Nat termination_by xs => xs /-- info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive []) - (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a + (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a✝ : List α), motive a✝ -/ #guard_msgs in #check foo.induct @@ -527,7 +527,7 @@ termination_by xs => xs /-- info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive []) - (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a + (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) : ∀ (a✝ : List α), motive a✝ -/ #guard_msgs in #check bar.induct @@ -545,7 +545,7 @@ termination_by n => n /-- info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive n.succ) - (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a + (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check foo.induct @@ -563,7 +563,7 @@ termination_by n => n /-- info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0)) (case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0)) - (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) : ∀ (a : Nat), motive a + (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check bar.induct @@ -585,14 +585,14 @@ end /-- info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) - (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a + (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a✝ : Nat), motive1 a✝ -/ #guard_msgs in #check even.induct /-- info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) - (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive2 a + (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a✝ : Nat), motive2 a✝ -/ #guard_msgs in #check odd.induct @@ -615,7 +615,7 @@ end /-- info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) - (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : ∀ (a : Tree), motive1 a + (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : ∀ (a✝ : Tree), motive1 a✝ -/ #guard_msgs in #check Tree.map.induct @@ -687,7 +687,7 @@ info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (c (case3 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 0), motive x x_1 0 a) (case4 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 1), motive x x_1 1 a) (case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a) : - ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2 + ∀ (a✝ a✝¹ k : Nat) (a✝² : Fin k), motive a✝ a✝¹ k a✝² -/ #guard_msgs in #check foo.induct @@ -739,7 +739,7 @@ termination_by n => n /-- info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), a = 23 → motive n.succ) (case3 : ¬a = 23 → motive a.succ) - (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) : ∀ (a : Nat), motive a + (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) : ∀ (a✝ : Nat), motive a✝ -/ #guard_msgs in #check foo.induct diff --git a/tests/lean/run/namePatEqThm.lean b/tests/lean/run/namePatEqThm.lean index a618088387fa..043ffd41e4a8 100644 --- a/tests/lean/run/namePatEqThm.lean +++ b/tests/lean/run/namePatEqThm.lean @@ -27,9 +27,8 @@ info: f.eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: /-- info: f.eq_3 : - ∀ (x : List Nat), - (∀ (x_1 y : Nat), x = [x_1, y] → False) → - (∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], []) + ∀ (x✝ : List Nat) (x_2 : ∀ (x y : Nat), x✝ = [x, y] → False) + (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: y :: zs → False), f x✝ = ([], []) -/ #guard_msgs in #check f.eq_3 diff --git a/tests/lean/run/reserved.lean b/tests/lean/run/reserved.lean index 97540a421c6e..83e2c90b7c74 100644 --- a/tests/lean/run/reserved.lean +++ b/tests/lean/run/reserved.lean @@ -41,9 +41,9 @@ def nonrecfun : Bool → Nat /-- info: nonrecfun.eq_def : - ∀ (x : Bool), - nonrecfun x = - match x with + ∀ (x✝ : Bool), + nonrecfun x✝ = + match x✝ with | false => 0 | true => 0 -/ @@ -64,9 +64,9 @@ def fact : Nat → Nat /-- info: fact.eq_def : - ∀ (x : Nat), - fact x = - match x with + ∀ (x✝ : Nat), + fact x✝ = + match x✝ with | 0 => 1 | n.succ => (n + 1) * fact n -/ diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index 63d7f0a4337c..5c677ec7dc72 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -631,7 +631,7 @@ namespace FunIndTests info: A.size.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self) (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty) (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a)) - (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a + (case6 : motive_2 B.empty) : ∀ (a✝ : A), motive_1 a✝ -/ #guard_msgs in #check A.size.induct @@ -649,7 +649,7 @@ info: A.subs.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A → Prop) (case1 : ∀ (a : MutualIndNonMutualFun.A), motive a → motive a.self) (case2 : ∀ (a : MutualIndNonMutualFun.B), motive (MutualIndNonMutualFun.A.other a)) - (case3 : motive MutualIndNonMutualFun.A.empty) : ∀ (a : MutualIndNonMutualFun.A), motive a + (case3 : motive MutualIndNonMutualFun.A.empty) : ∀ (a✝ : MutualIndNonMutualFun.A), motive a✝ -/ #guard_msgs in #check MutualIndNonMutualFun.A.self_size.induct @@ -659,7 +659,7 @@ info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → Mutu (case1 : ∀ (n : Nat) (a : MutualIndNonMutualFun.A), motive n a → motive n a.self) (case2 : ∀ (x : Nat) (a : MutualIndNonMutualFun.B), motive x (MutualIndNonMutualFun.A.other a)) (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) : - ∀ (a : Nat) (a_1 : MutualIndNonMutualFun.A), motive a a_1 + ∀ (a✝ : Nat) (a✝¹ : MutualIndNonMutualFun.A), motive a✝ a✝¹ -/ #guard_msgs in #check MutualIndNonMutualFun.A.self_size_with_param.induct @@ -668,7 +668,7 @@ info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → Mutu info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self) (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty) (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a)) - (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a + (case6 : motive_2 B.empty) : ∀ (a✝ : A), motive_1 a✝ -/ #guard_msgs in #check A.hasNoBEmpty.induct @@ -676,7 +676,7 @@ info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case /-- info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1 0) (case2 : ∀ (n : Nat), motive_2 n → motive_1 n.succ) (case3 : motive_2 0) - (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a + (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a✝ : Nat), motive_1 a✝ -/ #guard_msgs in #check EvenOdd.isEven.induct diff --git a/tests/lean/run/unfoldLemma.lean b/tests/lean/run/unfoldLemma.lean index 01cb1d88a229..38f34907f1d0 100644 --- a/tests/lean/run/unfoldLemma.lean +++ b/tests/lean/run/unfoldLemma.lean @@ -13,9 +13,9 @@ theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α /-- info: Option_map.eq_def.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : - ∀ (x : Option α), - Option_map f x = - match x with + ∀ (x✝ : Option α), + Option_map f x✝ = + match x✝ with | none => none | some x => some (f x) -/ diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean index 71e48766e6ce..a95218e5cb9e 100644 --- a/tests/lean/run/wfEqns5.lean +++ b/tests/lean/run/wfEqns5.lean @@ -15,9 +15,9 @@ theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x /-- info: foo.eq_def : - ∀ (x x_1 : Nat), - foo x x_1 = - match x, x_1 with + ∀ (x✝ x✝¹ : Nat), + foo x✝ x✝¹ = + match x✝, x✝¹ with | 0, m => match m with | 0 => 0 @@ -52,9 +52,9 @@ theorem bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x /-- info: bar.eq_def : - ∀ (x x_1 : Nat), - bar x x_1 = - match x, x_1 with + ∀ (x✝ x✝¹ : Nat), + bar x✝ x✝¹ = + match x✝, x✝¹ with | 0, m => match m with | 0 => 0 @@ -84,9 +84,9 @@ theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x /-- info: Structural.foo.eq_def : - ∀ (x x_1 : Nat), - foo x x_1 = - match x, x_1 with + ∀ (x✝ x✝¹ : Nat), + foo x✝ x✝¹ = + match x✝, x✝¹ with | 0, m => match m with | 0 => 0 @@ -121,9 +121,9 @@ theorem Structural.bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x /-- info: Structural.bar.eq_def : - ∀ (x x_1 : Nat), - bar x x_1 = - match x, x_1 with + ∀ (x✝ x✝¹ : Nat), + bar x✝ x✝¹ = + match x✝, x✝¹ with | 0, m => match m with | 0 => 0