From 4d1343d67005749367a08d2964a1dfb0bf09d3dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Jan 2022 17:23:34 -0800 Subject: [PATCH] chore: use `_eq` instead of `eq` to name auto generated equational theorems --- src/Lean/Elab/PreDefinition/Eqns.lean | 2 +- .../Elab/PreDefinition/Structural/Eqns.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 2 +- tests/lean/run/structuralEqns.lean | 36 +++++++++---------- tests/lean/run/structuralEqns2.lean | 10 +++--- tests/lean/run/structuralEqns3.lean | 4 +-- tests/lean/run/wfEqns1.lean | 4 +-- tests/lean/run/wfEqns2.lean | 10 +++--- tests/lean/run/wfEqns3.lean | 2 +- tests/lean/run/wfEqns4.lean | 8 ++--- 10 files changed, 40 insertions(+), 40 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index b2c05727de..cad43e8be4 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -111,7 +111,7 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ← /-- Create a "unique" base name for equations and splitter -/ def mkBaseNameFor (env : Environment) (declName : Name) : Name := - Lean.mkBaseNameFor env declName `eq_1 `_eqns + Lean.mkBaseNameFor env declName `_eq_1 `_eqns /-- Try to close goal using `rfl` with smart unfolding turned off. -/ def tryURefl (mvarId : MVarId) : MetaM Bool := diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index 495ad881ff..b247672233 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -64,7 +64,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) := for i in [: eqnTypes.size] do let type := eqnTypes[i] trace[Elab.definition.structural.eqns] "{eqnTypes[i]}" - let name := baseName ++ (`eq).appendIndexAfter (i+1) + let name := baseName ++ (`_eq).appendIndexAfter (i+1) thmNames := thmNames.push name let value ← mkProof info.declName type addDecl <| Declaration.thmDecl { diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 8d7d916193..d80c6ed71d 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -72,7 +72,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) := for i in [: eqnTypes.size] do let type := eqnTypes[i] trace[Elab.definition.wf.eqns] "{eqnTypes[i]}" - let name := baseName ++ (`eq).appendIndexAfter (i+1) + let name := baseName ++ (`_eq).appendIndexAfter (i+1) thmNames := thmNames.push name let value ← mkProof declName type addDecl <| Declaration.thmDecl { diff --git a/tests/lean/run/structuralEqns.lean b/tests/lean/run/structuralEqns.lean index e1a60763bd..eef32516ec 100644 --- a/tests/lean/run/structuralEqns.lean +++ b/tests/lean/run/structuralEqns.lean @@ -6,8 +6,8 @@ def tst (declName : Name) : MetaM Unit := do IO.println (← getEqnsFor? declName) #eval tst ``List.map -#check @List.map.eq_1 -#check @List.map.eq_2 +#check @List.map._eq_1 +#check @List.map._eq_2 def foo (xs ys zs : List Nat) : List Nat := match (xs, ys) with @@ -20,8 +20,8 @@ def foo (xs ys zs : List Nat) : List Nat := #eval tst ``foo -#check foo.eq_1 -#check foo.eq_2 +#check foo._eq_1 +#check foo._eq_2 #eval tst ``foo @@ -33,11 +33,11 @@ def g : List Nat → List Nat → Nat | x::xs, [] => g xs [] #eval tst ``g -#check g.eq_1 -#check g.eq_2 -#check g.eq_3 -#check g.eq_4 -#check g.eq_5 +#check g._eq_1 +#check g._eq_2 +#check g._eq_3 +#check g._eq_4 +#check g._eq_5 def h (xs : List Nat) (y : Nat) : Nat := match xs with @@ -48,9 +48,9 @@ def h (xs : List Nat) (y : Nat) : Nat := | y+1 => h xs y #eval tst ``h -#check h.eq_1 -#check h.eq_2 -#check h.eq_3 +#check h._eq_1 +#check h._eq_2 +#check h._eq_3 def r (i j : Nat) : Nat := i + @@ -62,9 +62,9 @@ def r (i j : Nat) : Nat := | Nat.succ j => r i j #eval tst ``r -#check r.eq_1 -#check r.eq_2 -#check r.eq_3 +#check r._eq_1 +#check r._eq_2 +#check r._eq_3 def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α := f i <| @@ -76,6 +76,6 @@ def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α := | Nat.succ j => bla f g a i j #eval tst ``bla -#check @bla.eq_1 -#check @bla.eq_2 -#check @bla.eq_3 +#check @bla._eq_1 +#check @bla._eq_2 +#check @bla._eq_3 diff --git a/tests/lean/run/structuralEqns2.lean b/tests/lean/run/structuralEqns2.lean index a2d3d73e87..9cbc1e6638 100644 --- a/tests/lean/run/structuralEqns2.lean +++ b/tests/lean/run/structuralEqns2.lean @@ -12,9 +12,9 @@ def g (i j : Nat) : Nat := | Nat.succ j => g i j #eval tst ``g -#check g.eq_1 -#check g.eq_2 -#check g.eq_3 +#check g._eq_1 +#check g._eq_2 +#check g._eq_3 def h (i j : Nat) : Nat := let z := @@ -24,5 +24,5 @@ def h (i j : Nat) : Nat := z + z #eval tst ``h -#check h.eq_1 -#check h.eq_2 +#check h._eq_1 +#check h._eq_2 diff --git a/tests/lean/run/structuralEqns3.lean b/tests/lean/run/structuralEqns3.lean index 3e568ac8bc..2f97b830ee 100644 --- a/tests/lean/run/structuralEqns3.lean +++ b/tests/lean/run/structuralEqns3.lean @@ -15,5 +15,5 @@ def wk_comp : Wk n m → Wk m l → Wk n l #eval tst ``wk_comp -#check @wk_comp.eq_1 -#check @wk_comp.eq_2 +#check @wk_comp._eq_1 +#check @wk_comp._eq_2 diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean index 98c8cb685f..4011d29193 100644 --- a/tests/lean/run/wfEqns1.lean +++ b/tests/lean/run/wfEqns1.lean @@ -23,5 +23,5 @@ decreasing_by #print isEven #eval tst ``isEven -#check @isEven.eq_1 -#check @isEven.eq_2 +#check @isEven._eq_1 +#check @isEven._eq_2 diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean index f3ebd00b2a..8d4c4d3ba3 100644 --- a/tests/lean/run/wfEqns2.lean +++ b/tests/lean/run/wfEqns2.lean @@ -31,9 +31,9 @@ decreasing_by decide #eval tst ``g -#check g.eq_1 -#check g.eq_2 -#check g.eq_3 +#check g._eq_1 +#check g._eq_2 +#check g._eq_3 #eval tst ``h -#check h.eq_1 -#check h.eq_2 +#check h._eq_1 +#check h._eq_2 diff --git a/tests/lean/run/wfEqns3.lean b/tests/lean/run/wfEqns3.lean index f4c1a2c10c..38f6ddffeb 100644 --- a/tests/lean/run/wfEqns3.lean +++ b/tests/lean/run/wfEqns3.lean @@ -16,4 +16,4 @@ decreasing_by exact h #eval tst ``f -#check f.eq_1 +#check f._eq_1 diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean index d65dae7f2f..8a5e8c5faf 100644 --- a/tests/lean/run/wfEqns4.lean +++ b/tests/lean/run/wfEqns4.lean @@ -36,9 +36,9 @@ decreasing_by #eval f 5 'a' 'b' #eval tst ``f -#check @f.eq_1 -#check @f.eq_2 +#check @f._eq_1 +#check @f._eq_2 #eval tst ``h -#check @h.eq_1 -#check @h.eq_2 +#check @h._eq_1 +#check @h._eq_2