From 20038140853cf121d401d281bd30bbcee871797d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 13 Mar 2024 00:56:27 -0700
Subject: [PATCH] chore: rename automatically generated equational theorems
 (#3661)

cc @nomeata
---
 RELEASES.md                                   | 27 +++++++++++
 src/Lean/Elab/PreDefinition/Eqns.lean         |  2 +-
 .../Elab/PreDefinition/Structural/Eqns.lean   |  2 +-
 src/Lean/Elab/PreDefinition/WF/Eqns.lean      |  2 +-
 src/Lean/Meta/Tactic/Simp/Types.lean          |  2 +-
 tests/lean/1026.lean.expected.out             |  9 ----
 tests/lean/1074a.lean.expected.out            |  4 --
 tests/lean/974.lean                           | 20 --------
 tests/lean/974.lean.expected.out              |  9 ----
 tests/lean/986.lean                           |  4 --
 tests/lean/986.lean.expected.out              |  9 ----
 tests/lean/eqValue.lean                       | 11 -----
 tests/lean/eqValue.lean.expected.out          |  4 --
 tests/lean/heapSort.lean.expected.out         | 17 -------
 tests/lean/namePatEqThm.lean                  | 15 ------
 tests/lean/namePatEqThm.lean.expected.out     |  8 ----
 tests/lean/{ => run}/1026.lean                | 12 ++++-
 tests/lean/{ => run}/1074a.lean               |  9 +++-
 tests/lean/run/1080.lean                      |  4 +-
 tests/lean/run/974.lean                       | 40 ++++++++++++++++
 tests/lean/run/986.lean                       | 19 ++++++++
 tests/lean/run/byteSliceIssue.lean            |  2 +-
 tests/lean/run/eqValue.lean                   | 21 +++++++++
 tests/lean/run/eqnsAtSimp3.lean               |  4 +-
 tests/lean/{ => run}/heapSort.lean            | 13 +++++-
 tests/lean/run/instEtaIssue.lean              |  4 +-
 tests/lean/run/match_lit_fin_cover.lean       | 20 ++++----
 tests/lean/run/match_lit_issues.lean          | 20 ++++----
 tests/lean/run/namePatEqThm.lean              | 35 ++++++++++++++
 tests/lean/run/nestedIssueMatch.lean          |  4 +-
 tests/lean/run/nestedWF.lean                  | 14 +++---
 tests/lean/run/overAndPartialAppsAtWF.lean    |  2 +-
 tests/lean/run/printEqns.lean                 | 14 +++---
 tests/lean/run/robinson.lean                  |  8 ++--
 tests/lean/run/rossel1.lean                   |  6 +--
 tests/lean/run/simpAtDefIssue.lean            |  8 ++--
 tests/lean/run/simp_eqn_bug.lean              |  6 +--
 tests/lean/run/splitIssue.lean                |  8 ++--
 tests/lean/run/splitList.lean                 | 16 +++----
 tests/lean/run/streamEqIssue.lean             |  6 +--
 .../structEqns.lean}                          | 23 +++++++++-
 tests/lean/run/structuralEqns.lean            | 46 +++++++++----------
 tests/lean/run/structuralEqns2.lean           | 12 ++---
 tests/lean/run/structuralEqns3.lean           |  6 +--
 tests/lean/run/wfEqns1.lean                   |  6 +--
 tests/lean/run/wfEqns2.lean                   | 12 ++---
 tests/lean/run/wfEqns3.lean                   |  4 +-
 tests/lean/run/wfEqns4.lean                   | 12 ++---
 tests/lean/structuralEqns.lean.expected.out   | 15 ------
 49 files changed, 321 insertions(+), 255 deletions(-)
 delete mode 100644 tests/lean/1026.lean.expected.out
 delete mode 100644 tests/lean/1074a.lean.expected.out
 delete mode 100644 tests/lean/974.lean
 delete mode 100644 tests/lean/974.lean.expected.out
 delete mode 100644 tests/lean/986.lean
 delete mode 100644 tests/lean/986.lean.expected.out
 delete mode 100644 tests/lean/eqValue.lean
 delete mode 100644 tests/lean/eqValue.lean.expected.out
 delete mode 100644 tests/lean/heapSort.lean.expected.out
 delete mode 100644 tests/lean/namePatEqThm.lean
 delete mode 100644 tests/lean/namePatEqThm.lean.expected.out
 rename tests/lean/{ => run}/1026.lean (55%)
 rename tests/lean/{ => run}/1074a.lean (69%)
 create mode 100644 tests/lean/run/974.lean
 create mode 100644 tests/lean/run/eqValue.lean
 rename tests/lean/{ => run}/heapSort.lean (95%)
 create mode 100644 tests/lean/run/namePatEqThm.lean
 rename tests/lean/{structuralEqns.lean => run/structEqns.lean} (55%)
 delete mode 100644 tests/lean/structuralEqns.lean.expected.out

diff --git a/RELEASES.md b/RELEASES.md
index 18b6753801..e6c7e073dd 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -31,6 +31,33 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+Breaking changes:
+
+* Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
+```
+def fact : Nat → Nat
+  | 0 => 1
+  | n+1 => (n+1) * fact n
+
+theorem ex : fact 0 = 1 := by unfold fact; decide
+
+#check fact.eq_1
+-- fact.eq_1 : fact 0 = 1
+
+#check fact.eq_2
+-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n
+
+#check fact.def
+/-
+fact.def :
+  ∀ (x : Nat),
+    fact x =
+      match x with
+      | 0 => 1
+      | Nat.succ n => (n + 1) * fact n
+-/
+```
+
 v4.7.0
 ---------
 
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 2a2eadd1b4..e0cc1c4f05 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -380,7 +380,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := baseName ++ `_unfold
+      let name := baseName ++ `def
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index 6738dddb6b..5ee888c748 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -68,7 +68,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
     let (type, value) ← removeUnusedEqnHypotheses type value
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index e0c71d28fa..f4e6b35808 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -117,7 +117,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
     let (type, value) ← removeUnusedEqnHypotheses type value
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 659effcec3..2540eb529f 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -285,7 +285,7 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
   /-
-  If `thmId` is an equational theorem (e.g., `foo._eq_1`), we should record `foo` instead.
+  If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
   See issue #3547.
   -/
   let thmId ← match thmId with
diff --git a/tests/lean/1026.lean.expected.out b/tests/lean/1026.lean.expected.out
deleted file mode 100644
index 64966ecc9a..0000000000
--- a/tests/lean/1026.lean.expected.out
+++ /dev/null
@@ -1,9 +0,0 @@
-1026.lean:1:4-1:7: warning: declaration uses 'sorry'
-1026.lean:9:8-9:10: warning: declaration uses 'sorry'
-foo._unfold (n : Nat) :
-  foo n =
-    if n = 0 then 0
-    else
-      let x := n - 1;
-      let_fun this := foo.proof_4;
-      foo x
diff --git a/tests/lean/1074a.lean.expected.out b/tests/lean/1074a.lean.expected.out
deleted file mode 100644
index f5b7e7683e..0000000000
--- a/tests/lean/1074a.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-Brx.interp._eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
-  Brx.interp H_2 =
-    match ⋯ with
-    | ⋯ => Brx.interp Hz
diff --git a/tests/lean/974.lean b/tests/lean/974.lean
deleted file mode 100644
index 0be5d5203b..0000000000
--- a/tests/lean/974.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-inductive Formula : Nat → Type u
-| bot                            : Formula n
-| imp (f₁ f₂ : Formula     n   ) : Formula n
-| all (f     : Formula    (n+1)) : Formula n
-
-def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
-| _, imp f₁ f₂ => f₁.count_quantifiers + f₂.count_quantifiers
-| _, all f => f.count_quantifiers + 1
-| _, _ => 0
-
-attribute [simp] Formula.count_quantifiers
-
-#check Formula.count_quantifiers._eq_1
-#check Formula.count_quantifiers._eq_2
-#check Formula.count_quantifiers._eq_3
-
-@[simp] def Formula.count_quantifiers2 : Formula n → Nat
-| imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2
-| all f     => f.count_quantifiers2 + 1
-| _         => 0
diff --git a/tests/lean/974.lean.expected.out b/tests/lean/974.lean.expected.out
deleted file mode 100644
index afc0622e0a..0000000000
--- a/tests/lean/974.lean.expected.out
+++ /dev/null
@@ -1,9 +0,0 @@
-Formula.count_quantifiers._eq_1.{u_1} :
-  ∀ (x : Nat) (f₁ f₂ : Formula x),
-    Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
-Formula.count_quantifiers._eq_2.{u_1} :
-  ∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1
-Formula.count_quantifiers._eq_3.{u_1} :
-  ∀ (x : Nat) (x_1 : Formula x),
-    (∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) →
-      (∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0
diff --git a/tests/lean/986.lean b/tests/lean/986.lean
deleted file mode 100644
index b5ba6793e2..0000000000
--- a/tests/lean/986.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-attribute [simp] Array.insertionSort.swapLoop
-
-#check Array.insertionSort.swapLoop._eq_1
-#check Array.insertionSort.swapLoop._eq_2
diff --git a/tests/lean/986.lean.expected.out b/tests/lean/986.lean.expected.out
deleted file mode 100644
index 885bd531d5..0000000000
--- a/tests/lean/986.lean.expected.out
+++ /dev/null
@@ -1,9 +0,0 @@
-Array.insertionSort.swapLoop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a) :
-  Array.insertionSort.swapLoop lt a 0 h = a
-Array.insertionSort.swapLoop._eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
-  (h : Nat.succ j' < Array.size a) :
-  Array.insertionSort.swapLoop lt a (Nat.succ j') h =
-    let_fun h' := ⋯;
-    if lt a[Nat.succ j'] a[j'] = true then
-      Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' ⋯
-    else a
diff --git a/tests/lean/eqValue.lean b/tests/lean/eqValue.lean
deleted file mode 100644
index 2ccbcc4bfc..0000000000
--- a/tests/lean/eqValue.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-@[simp] def f (x : Nat) : Nat :=
-  match x with
-  | 0    => 1
-  | 100  => 2
-  | 1000 => 3
-  | x+1  => f x
-
-#check f._eq_1
-#check f._eq_2
-#check f._eq_3
-#check f._eq_4
diff --git a/tests/lean/eqValue.lean.expected.out b/tests/lean/eqValue.lean.expected.out
deleted file mode 100644
index 05601457a8..0000000000
--- a/tests/lean/eqValue.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-f._eq_1 : f 0 = 1
-f._eq_2 : f 100 = 2
-f._eq_3 : f 1000 = 3
-f._eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f (Nat.succ x_2) = f x_2
diff --git a/tests/lean/heapSort.lean.expected.out b/tests/lean/heapSort.lean.expected.out
deleted file mode 100644
index 9e0ab4f588..0000000000
--- a/tests/lean/heapSort.lean.expected.out
+++ /dev/null
@@ -1,17 +0,0 @@
-heapSort.lean:15:4-15:15: warning: declaration uses 'sorry'
-heapSort.lean:15:4-15:15: warning: declaration uses 'sorry'
-heapSort.lean:15:4-15:15: warning: declaration uses 'sorry'
-heapSort.lean:43:4-43:10: warning: declaration uses 'sorry'
-heapSort.lean:58:4-58:13: warning: declaration uses 'sorry'
-heapSort.lean:58:4-58:13: warning: declaration uses 'sorry'
-heapSort.lean:58:4-58:13: warning: declaration uses 'sorry'
-heapSort.lean:102:4-102:13: warning: declaration uses 'sorry'
-heapSort.lean:102:4-102:13: warning: declaration uses 'sorry'
-Array.heapSort.loop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y)
-  (out : Array α) :
-  Array.heapSort.loop lt a out =
-    match e : BinaryHeap.max a with
-    | none => out
-    | some x =>
-      let_fun this := ⋯;
-      Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)
diff --git a/tests/lean/namePatEqThm.lean b/tests/lean/namePatEqThm.lean
deleted file mode 100644
index 18c1185082..0000000000
--- a/tests/lean/namePatEqThm.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-@[simp] def iota : Nat → List Nat
-  | 0       => []
-  | m@(n+1) => m :: iota n
-
-#check iota._eq_1
-#check iota._eq_2
-
-@[simp] def f : List Nat → List Nat × List Nat
- | xs@(x :: ys@(y :: [])) => (xs, ys)
- | xs@(x :: ys@(y :: zs)) => f zs
- | _ => ([], [])
-
-#check f._eq_1
-#check f._eq_2
-#check f._eq_3
diff --git a/tests/lean/namePatEqThm.lean.expected.out b/tests/lean/namePatEqThm.lean.expected.out
deleted file mode 100644
index 73e55b147d..0000000000
--- a/tests/lean/namePatEqThm.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-iota._eq_1 : iota 0 = []
-iota._eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n
-f._eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y])
-f._eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs
-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 = ([], [])
diff --git a/tests/lean/1026.lean b/tests/lean/run/1026.lean
similarity index 55%
rename from tests/lean/1026.lean
rename to tests/lean/run/1026.lean
index afe792b156..ec06a943ef 100644
--- a/tests/lean/1026.lean
+++ b/tests/lean/run/1026.lean
@@ -10,4 +10,14 @@ theorem ex : foo 0 = 0 := by
   unfold foo
   sorry
 
-#check foo._unfold
+/--
+info: foo.def (n : Nat) :
+  foo n =
+    if n = 0 then 0
+    else
+      let x := n - 1;
+      let_fun this := foo.proof_4;
+      foo x
+-/
+#guard_msgs in
+#check foo.def
diff --git a/tests/lean/1074a.lean b/tests/lean/run/1074a.lean
similarity index 69%
rename from tests/lean/1074a.lean
rename to tests/lean/run/1074a.lean
index 49451e8026..3e5e1c9d9e 100644
--- a/tests/lean/1074a.lean
+++ b/tests/lean/run/1074a.lean
@@ -18,4 +18,11 @@ def Brx.interp_nil (H: Brx a): H.interp = H.interp
     rfl
   }
 
-#check Brx.interp._eq_1
+/--
+info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
+  Brx.interp H_2 =
+    match ⋯ with
+    | ⋯ => Brx.interp Hz
+-/
+#guard_msgs in
+#check Brx.interp.eq_1
diff --git a/tests/lean/run/1080.lean b/tests/lean/run/1080.lean
index e4132a9d86..265be5849b 100644
--- a/tests/lean/run/1080.lean
+++ b/tests/lean/run/1080.lean
@@ -17,8 +17,8 @@ def Bar.check: Bar f → Prop
 
 attribute [simp] Bar.check
 
-#check Bar.check._eq_1
-#check Bar.check._eq_2
+#check Bar.check.eq_1
+#check Bar.check.eq_2
 #check Bar.check.match_1.eq_1
 #check Bar.check.match_1.eq_2
 #check Bar.check.match_1.splitter
diff --git a/tests/lean/run/974.lean b/tests/lean/run/974.lean
new file mode 100644
index 0000000000..0077bac03a
--- /dev/null
+++ b/tests/lean/run/974.lean
@@ -0,0 +1,40 @@
+inductive Formula : Nat → Type u where
+  | bot                            : Formula n
+  | imp (f₁ f₂ : Formula     n   ) : Formula n
+  | all (f     : Formula    (n+1)) : Formula n
+
+def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
+  | _, imp f₁ f₂ => f₁.count_quantifiers + f₂.count_quantifiers
+  | _, all f => f.count_quantifiers + 1
+  | _, _ => 0
+
+attribute [simp] Formula.count_quantifiers
+
+/--
+info: Formula.count_quantifiers.eq_1.{u_1} :
+  ∀ (x : Nat) (f₁ f₂ : Formula x),
+    Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
+-/
+#guard_msgs in
+#check Formula.count_quantifiers.eq_1
+
+/--
+info: Formula.count_quantifiers.eq_2.{u_1} :
+  ∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 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 = Formula.imp f₁ f₂ → False) →
+      (∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0
+-/
+#guard_msgs in
+#check Formula.count_quantifiers.eq_3
+
+@[simp] def Formula.count_quantifiers2 : Formula n → Nat
+  | imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2
+  | all f     => f.count_quantifiers2 + 1
+  | _         => 0
diff --git a/tests/lean/run/986.lean b/tests/lean/run/986.lean
index 1448c57b97..1d7dc33fe1 100644
--- a/tests/lean/run/986.lean
+++ b/tests/lean/run/986.lean
@@ -1 +1,20 @@
 attribute [simp] Array.insertionSort.swapLoop
+
+/--
+info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a) :
+  Array.insertionSort.swapLoop lt a 0 h = a
+-/
+#guard_msgs in
+#check Array.insertionSort.swapLoop.eq_1
+
+/--
+info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
+  (h : Nat.succ j' < Array.size a) :
+  Array.insertionSort.swapLoop lt a (Nat.succ j') h =
+    let_fun h' := ⋯;
+    if lt a[Nat.succ j'] a[j'] = true then
+      Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' ⋯
+    else a
+-/
+#guard_msgs in
+#check Array.insertionSort.swapLoop.eq_2
diff --git a/tests/lean/run/byteSliceIssue.lean b/tests/lean/run/byteSliceIssue.lean
index 76147a5c2f..4d23883658 100644
--- a/tests/lean/run/byteSliceIssue.lean
+++ b/tests/lean/run/byteSliceIssue.lean
@@ -42,4 +42,4 @@ def forIn.loop [Monad m] (f : UInt8 → β → m (ForInStep β))
 termination_by _end - i
 
 attribute [simp] ByteSlice.forIn.loop
-#check @ByteSlice.forIn.loop._eq_1
+#check @ByteSlice.forIn.loop.eq_1
diff --git a/tests/lean/run/eqValue.lean b/tests/lean/run/eqValue.lean
new file mode 100644
index 0000000000..1e62bc1fab
--- /dev/null
+++ b/tests/lean/run/eqValue.lean
@@ -0,0 +1,21 @@
+@[simp] def f (x : Nat) : Nat :=
+  match x with
+  | 0    => 1
+  | 100  => 2
+  | 1000 => 3
+  | x+1  => f x
+
+/-- info: f.eq_1 : f 0 = 1 -/
+#guard_msgs in
+#check f.eq_1
+/-- info: f.eq_2 : f 100 = 2 -/
+#guard_msgs in
+#check f.eq_2
+/-- info: f.eq_3 : f 1000 = 3 -/
+#guard_msgs in
+#check f.eq_3
+/--
+info: f.eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f (Nat.succ x_2) = f x_2
+-/
+#guard_msgs in
+#check f.eq_4
diff --git a/tests/lean/run/eqnsAtSimp3.lean b/tests/lean/run/eqnsAtSimp3.lean
index d634112389..f38d5c73d5 100644
--- a/tests/lean/run/eqnsAtSimp3.lean
+++ b/tests/lean/run/eqnsAtSimp3.lean
@@ -38,7 +38,7 @@ theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z
   | x+1, y, z => 2 * f2 x y z
 
 
-#check f2._eq_4
+#check f2.eq_4
 
 theorem ex4 (x y z : Nat) (h : y = 5 → z = 6 → False) : ∃ w, f2 (x+1) y z = 2 * w := by
   simp [f2, h]
@@ -64,7 +64,7 @@ theorem ex6 (x y z : Nat) (h2 : z ≠ 6) : ∃ w, f2 (x+1) y z = 2 * w := by
   | x+1, 6, 4 => 3 * f3 x 0 1
   | x+1, y, z => 2 * f3 x y z
 
-#check f3._eq_5
+#check f3.eq_5
 
 theorem ex7 (x y z : Nat) (h2 : z ≠ 6) (h3 : y ≠ 6) : ∃ w, f3 (x+1) y z = 2 * w := by
   simp [f3, h2,  h3]
diff --git a/tests/lean/heapSort.lean b/tests/lean/run/heapSort.lean
similarity index 95%
rename from tests/lean/heapSort.lean
rename to tests/lean/run/heapSort.lean
index f252f73bf6..58f7f81571 100644
--- a/tests/lean/heapSort.lean
+++ b/tests/lean/run/heapSort.lean
@@ -173,6 +173,17 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
   loop (a.toBinaryHeap gt) #[]
 
 attribute [simp] Array.heapSort.loop
-#check Array.heapSort.loop._eq_1
+
+/--
+info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α) :
+  Array.heapSort.loop lt a out =
+    match e : BinaryHeap.max a with
+    | none => out
+    | some x =>
+      let_fun this := ⋯;
+      Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)
+-/
+#guard_msgs in
+#check Array.heapSort.loop.eq_1
 
 attribute [simp] BinaryHeap.heapifyDown
diff --git a/tests/lean/run/instEtaIssue.lean b/tests/lean/run/instEtaIssue.lean
index 27f18680fe..95414a15bc 100644
--- a/tests/lean/run/instEtaIssue.lean
+++ b/tests/lean/run/instEtaIssue.lean
@@ -8,12 +8,12 @@ attribute [simp] filter
 set_option pp.explicit true
 
 /--
-info: filter._eq_2.{u_1} {α : Type u_1} (p : α → Prop) [@DecidablePred α p] (x : α) (xs' : List α) :
+info: filter.eq_2.{u_1} {α : Type u_1} (p : α → Prop) [@DecidablePred α p] (x : α) (xs' : List α) :
   @Eq (List α) (@filter α p inst✝ (@List.cons α x xs'))
     (@ite (List α) (p x) (inst✝ x) (@List.cons α x (@filter α p inst✝ xs')) (@filter α p inst✝ xs'))
 -/
 #guard_msgs in
-#check filter._eq_2 -- We should not have terms of the form `@filter α p (fun x => inst✝ x) xs'`
+#check filter.eq_2 -- We should not have terms of the form `@filter α p (fun x => inst✝ x) xs'`
 
 
 def filter_length (p : α → Prop) [DecidablePred p] : (filter p xs).length ≤ xs.length := by
diff --git a/tests/lean/run/match_lit_fin_cover.lean b/tests/lean/run/match_lit_fin_cover.lean
index ed219a99ca..53353cc4d5 100644
--- a/tests/lean/run/match_lit_fin_cover.lean
+++ b/tests/lean/run/match_lit_fin_cover.lean
@@ -17,16 +17,16 @@ def boo (x : Fin 3) : Nat :=
   | 2, y+1 => bla x y + 1
 
 /--
-info: bla._eq_1 (y : Nat) : bla 0 y = 10
+info: bla.eq_1 (y : Nat) : bla 0 y = 10
 -/
 #guard_msgs in
-#check bla._eq_1
+#check bla.eq_1
 
 /--
-info: bla._eq_4 (y_2 : Nat) : bla 2 (Nat.succ y_2) = bla 2 y_2 + 1
+info: bla.eq_4 (y_2 : Nat) : bla 2 (Nat.succ y_2) = bla 2 y_2 + 1
 -/
 #guard_msgs in
-#check bla._eq_4
+#check bla.eq_4
 
 open BitVec
 
@@ -56,19 +56,19 @@ def foo' (x : BitVec 3) (y : Nat) : Nat :=
 attribute [simp] foo'
 
 /--
-info: foo'._eq_1 (y : Nat) : foo' (0#3) y = 7
+info: foo'.eq_1 (y : Nat) : foo' (0#3) y = 7
 -/
 #guard_msgs in
-#check foo'._eq_1
+#check foo'.eq_1
 
 /--
-info: foo'._eq_2 (y : Nat) : foo' (1#3) y = 6
+info: foo'.eq_2 (y : Nat) : foo' (1#3) y = 6
 -/
 #guard_msgs in
-#check foo'._eq_2
+#check foo'.eq_2
 
 /--
-info: foo'._eq_9 (y_2 : Nat) : foo' (7#3) (Nat.succ y_2) = foo' 7 y_2 + 1
+info: foo'.eq_9 (y_2 : Nat) : foo' (7#3) (Nat.succ y_2) = foo' 7 y_2 + 1
 -/
 #guard_msgs in
-#check foo'._eq_9
+#check foo'.eq_9
diff --git a/tests/lean/run/match_lit_issues.lean b/tests/lean/run/match_lit_issues.lean
index 14b434e38e..7df72feb77 100644
--- a/tests/lean/run/match_lit_issues.lean
+++ b/tests/lean/run/match_lit_issues.lean
@@ -4,8 +4,8 @@
   | _,  0  => b+1
   | _, a+1 => f1 (i-1) a (b*2)
 
-#check f1._eq_1
-#check f1._eq_2
+#check f1.eq_1
+#check f1.eq_2
 
 example : f1 (-1) a b = b := by simp -- should work
 example : f1 (-2) 0 b = b+1 := by simp
@@ -29,8 +29,8 @@ example (h : c ≠ 'a') : f2 c (a+1) b = f2 c a (b*2) := by simp
   | _,  0  => b+1
   | _, a+1 => f3 (i+1) a (b*2)
 
-#check f3._eq_1
-#check f3._eq_2
+#check f3.eq_1
+#check f3.eq_2
 
 example : f3 2 a b = b   := by simp -- should work
 example : f3 3 0 b = b+1 := by simp
@@ -43,8 +43,8 @@ example (h : i ≠ 2) : f3 i (a+1) b = f3 (i+1) a (b*2) := by simp; done -- shou
   | _,  0  => b+1
   | _, a+1 => f4 (i+1) a (b*2)
 
-#check f4._eq_1
-#check f4._eq_2
+#check f4.eq_1
+#check f4.eq_2
 
 example : f4 2 a b = b   := by simp -- should work
 example : f4 3 0 b = b+1 := by simp
@@ -57,8 +57,8 @@ example (h : i ≠ 2) : f4 i (a+1) b = f4 (i+1) a (b*2) := by simp -- should wor
   | _,  0  => b+1
   | _, a+1 => f5 (i+1) a (b*2)
 
-#check f5._eq_1
-#check f5._eq_2
+#check f5.eq_1
+#check f5.eq_2
 
 open BitVec
 
@@ -76,8 +76,8 @@ example (h : i ≠ 2#8) : f5 i (a+1) b = f5 (i+1) a (b*2) := by simp -- should w
   | _,  0  => b+1
   | _, a+1 => f6 (i+1) a (b*2)
 
-#check f6._eq_1
-#check f6._eq_2
+#check f6.eq_1
+#check f6.eq_2
 
 example : f6 2#8 a b = b   := by simp -- should work
 example : f6 2#8 a b = b   := by simp -- should work
diff --git a/tests/lean/run/namePatEqThm.lean b/tests/lean/run/namePatEqThm.lean
new file mode 100644
index 0000000000..8a627ebeee
--- /dev/null
+++ b/tests/lean/run/namePatEqThm.lean
@@ -0,0 +1,35 @@
+@[simp] def iota : Nat → List Nat
+  | 0       => []
+  | m@(n+1) => m :: iota n
+
+/-- info: iota.eq_1 : iota 0 = [] -/
+#guard_msgs in
+#check iota.eq_1
+
+/-- info: iota.eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n -/
+#guard_msgs in
+#check iota.eq_2
+
+@[simp] def f : List Nat → List Nat × List Nat
+ | xs@(x :: ys@(y :: [])) => (xs, ys)
+ | xs@(x :: ys@(y :: zs)) => f zs
+ | _ => ([], [])
+
+/-- info: f.eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y]) -/
+#guard_msgs in
+#check f.eq_1
+
+/--
+info: f.eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs
+-/
+#guard_msgs in
+#check f.eq_2
+
+/--
+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 = ([], [])
+-/
+#guard_msgs in
+#check f.eq_3
diff --git a/tests/lean/run/nestedIssueMatch.lean b/tests/lean/run/nestedIssueMatch.lean
index 5b0ac54b41..a1eccc46b3 100644
--- a/tests/lean/run/nestedIssueMatch.lean
+++ b/tests/lean/run/nestedIssueMatch.lean
@@ -9,8 +9,8 @@ decreasing_by all_goals sorry
 
 attribute [simp] g
 
-#check g._eq_1
-#check g._eq_2
+#check g.eq_1
+#check g.eq_2
 
 theorem ex3 : g (n + 1) = match g n with
     | 0 => 0
diff --git a/tests/lean/run/nestedWF.lean b/tests/lean/run/nestedWF.lean
index 8caabf2b7d..7fea4e10d8 100644
--- a/tests/lean/run/nestedWF.lean
+++ b/tests/lean/run/nestedWF.lean
@@ -28,12 +28,12 @@ attribute [simp] g
 attribute [simp] h
 attribute [simp] f
 
-#check g._eq_1
-#check g._eq_2
+#check g.eq_1
+#check g.eq_2
 
-#check h._eq_1
+#check h.eq_1
 
-#check f._eq_1
+#check f.eq_1
 
 end Ex1
 
@@ -51,14 +51,14 @@ decreasing_by all_goals sorry
 theorem ex1 : g 0 = 0 := by
   rw [g]
 
-#check g._eq_1
-#check g._eq_2
+#check g.eq_1
+#check g.eq_2
 
 theorem ex2 : g 0 = 0 := by
   unfold g
   simp
 
-#check g._unfold
+#check g.def
 
 
 end Ex2
diff --git a/tests/lean/run/overAndPartialAppsAtWF.lean b/tests/lean/run/overAndPartialAppsAtWF.lean
index 6ff6a3269a..72110a402a 100644
--- a/tests/lean/run/overAndPartialAppsAtWF.lean
+++ b/tests/lean/run/overAndPartialAppsAtWF.lean
@@ -19,4 +19,4 @@ termination_by _ _ _ => a.size - i
     (· + y)
 termination_by x
 
-#check f._eq_1
+#check f.eq_1
diff --git a/tests/lean/run/printEqns.lean b/tests/lean/run/printEqns.lean
index c0a0d06c0b..887c6ad555 100644
--- a/tests/lean/run/printEqns.lean
+++ b/tests/lean/run/printEqns.lean
@@ -1,7 +1,7 @@
 /--
 info: equations:
-private theorem List.append._eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
+private theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
+private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
   List.append (a :: l) x = a :: List.append l x
 -/
 #guard_msgs in
@@ -9,8 +9,8 @@ private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α)
 
 /--
 info: equations:
-private theorem List.append._eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
+private theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
+private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
   List.append (a :: l) x = a :: List.append l x
 -/
 #guard_msgs in
@@ -23,9 +23,9 @@ private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α)
 
 /--
 info: equations:
-private theorem ack._eq_1 : ∀ (x : Nat), ack 0 x = x + 1
-private theorem ack._eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
-private theorem ack._eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
+private theorem ack.eq_1 : ∀ (x : Nat), ack 0 x = x + 1
+private theorem ack.eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
+private theorem ack.eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
 -/
 #guard_msgs in
 #print eqns ack
diff --git a/tests/lean/run/robinson.lean b/tests/lean/run/robinson.lean
index 2327bbc088..6f82a09e64 100644
--- a/tests/lean/run/robinson.lean
+++ b/tests/lean/run/robinson.lean
@@ -49,10 +49,10 @@ decreasing_by
 attribute [simp] robinson
 
 set_option pp.proofs true
-#check robinson._eq_1
-#check robinson._eq_2
-#check robinson._eq_3
-#check robinson._eq_4
+#check robinson.eq_1
+#check robinson.eq_2
+#check robinson.eq_3
+#check robinson.eq_4
 
 theorem ex : (robinson (Term.Var 0) (Term.Var 0)).1 = some id := by
   unfold robinson
diff --git a/tests/lean/run/rossel1.lean b/tests/lean/run/rossel1.lean
index a62747d956..57837d4b8d 100644
--- a/tests/lean/run/rossel1.lean
+++ b/tests/lean/run/rossel1.lean
@@ -21,9 +21,9 @@ def Lineage.container' {rtr i} : Lineage rtr i → (Option ID × Reactor)
 
 attribute [simp] Lineage.container'
 
-#check @Lineage.container'._eq_1
-#check @Lineage.container'._eq_2
-#check @Lineage.container'._eq_3
+#check @Lineage.container'.eq_1
+#check @Lineage.container'.eq_2
+#check @Lineage.container'.eq_3
 
 @[simp] def Lineage.container : Lineage rtr i → (Option ID × Reactor)
   | nested l@h:(nested ..) _ => l.container
diff --git a/tests/lean/run/simpAtDefIssue.lean b/tests/lean/run/simpAtDefIssue.lean
index e82f81f901..bae33f3308 100644
--- a/tests/lean/run/simpAtDefIssue.lean
+++ b/tests/lean/run/simpAtDefIssue.lean
@@ -5,7 +5,7 @@
   | x+1, 5 => 2 * g x 0
   | x+1, y => 2 * g x y
 
-#check g._eq_1
-#check g._eq_2
-#check g._eq_3
-#check g._eq_4
+#check g.eq_1
+#check g.eq_2
+#check g.eq_3
+#check g.eq_4
diff --git a/tests/lean/run/simp_eqn_bug.lean b/tests/lean/run/simp_eqn_bug.lean
index 22f62770eb..9871a9f8f5 100644
--- a/tests/lean/run/simp_eqn_bug.lean
+++ b/tests/lean/run/simp_eqn_bug.lean
@@ -5,6 +5,6 @@
    | []    => a
    | x::xs => x + f a xs
 
-example : f 25 xs = 0 := by apply f._eq_1
-example (h : a = 25 → False) : f a [] = a := by apply f._eq_2; assumption
-example (h : a = 25 → False) : f a (x::xs) = x + f a xs := by apply f._eq_3; assumption
+example : f 25 xs = 0 := by apply f.eq_1
+example (h : a = 25 → False) : f a [] = a := by apply f.eq_2; assumption
+example (h : a = 25 → False) : f a (x::xs) = x + f a xs := by apply f.eq_3; assumption
diff --git a/tests/lean/run/splitIssue.lean b/tests/lean/run/splitIssue.lean
index fe8b4cbdc7..143722e829 100644
--- a/tests/lean/run/splitIssue.lean
+++ b/tests/lean/run/splitIssue.lean
@@ -19,9 +19,9 @@ theorem len_nil : len ([] : List α) = 0 := by
   simp [len]
 
 -- The `simp [len]` above generated the following equation theorems for len
-#check @len._eq_1
-#check @len._eq_2
-#check @len._eq_3 -- It is conditional, and may be tricky to use.
+#check @len.eq_1
+#check @len.eq_2
+#check @len.eq_3 -- It is conditional, and may be tricky to use.
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
@@ -30,7 +30,7 @@ theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
 
 -- The `unfold` tactic above generated the following theorem
-#check @len._unfold
+#check @len.def
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index 239a791671..240ec95698 100644
--- a/tests/lean/run/splitList.lean
+++ b/tests/lean/run/splitList.lean
@@ -38,9 +38,9 @@ theorem len_nil : len ([] : List α) = 0 := by
  simp [len]
 
 -- The `simp [len]` above generated the following equation theorems for len
-#check @len._eq_1
-#check @len._eq_2
-#check @len._eq_3
+#check @len.eq_1
+#check @len.eq_2
+#check @len.eq_3
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
@@ -49,7 +49,7 @@ theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
 
 -- The `unfold` tactic above generated the following theorem
-#check @len._unfold
+#check @len.def
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -88,9 +88,9 @@ theorem len_nil : len ([] : List α) = 0 := by
   simp [len]
 
 -- The `simp [len]` above generated the following equation theorems for len
-#check @len._eq_1
-#check @len._eq_2
-#check @len._eq_3
+#check @len.eq_1
+#check @len.eq_2
+#check @len.eq_3
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
@@ -99,7 +99,7 @@ theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
 
 -- The `unfold` tactic above generated the following theorem
-#check @len._unfold
+#check @len.def
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
diff --git a/tests/lean/run/streamEqIssue.lean b/tests/lean/run/streamEqIssue.lean
index 6401c0016e..2174a73bf3 100644
--- a/tests/lean/run/streamEqIssue.lean
+++ b/tests/lean/run/streamEqIssue.lean
@@ -4,6 +4,6 @@
   | n + 1, some (_, s') => hasLength n s'
   | _, _ => false
 
-#check @Stream.hasLength._eq_1
-#check @Stream.hasLength._eq_2
-#check @Stream.hasLength._eq_3
+#check @Stream.hasLength.eq_1
+#check @Stream.hasLength.eq_2
+#check @Stream.hasLength.eq_3
diff --git a/tests/lean/structuralEqns.lean b/tests/lean/run/structEqns.lean
similarity index 55%
rename from tests/lean/structuralEqns.lean
rename to tests/lean/run/structEqns.lean
index 4bcb423ec9..f5842c62f8 100644
--- a/tests/lean/structuralEqns.lean
+++ b/tests/lean/run/structEqns.lean
@@ -15,11 +15,32 @@ def foo (xs ys zs : List Nat) : List Nat :=
      | _  => [2]
 
 #eval tst ``foo
-#check foo._unfold
+
+/--
+info: foo.def (xs ys zs : List Nat) :
+  foo xs ys zs =
+    match (xs, ys) with
+    | (xs', ys') =>
+      match zs with
+      | z :: zs => foo xs ys zs
+      | x =>
+        match ys' with
+        | [] => [1]
+        | x => [2]
+-/
+#guard_msgs in
+#check foo.def
 
 
 def bar (xs ys : List Nat) : List Nat :=
   match xs ++ [], ys ++ [] with
   | xs', ys'   => xs' ++ ys'
 
+/--
+info: def bar : List Nat → List Nat → List Nat :=
+fun xs ys =>
+  match xs ++ [], ys ++ [] with
+  | xs', ys' => xs' ++ ys'
+-/
+#guard_msgs in
 #print bar  -- should not contain either `let _discr` aux binding
diff --git a/tests/lean/run/structuralEqns.lean b/tests/lean/run/structuralEqns.lean
index f9e1892554..c3ace8752f 100644
--- a/tests/lean/run/structuralEqns.lean
+++ b/tests/lean/run/structuralEqns.lean
@@ -6,9 +6,9 @@ def tst (declName : Name) : MetaM Unit := do
   IO.println (← getUnfoldEqnFor? declName)
 
 #eval tst ``List.map
-#check @List.map._eq_1
-#check @List.map._eq_2
-#check @List.map._unfold
+#check @List.map.eq_1
+#check @List.map.eq_2
+#check @List.map.def
 
 def foo (xs ys zs : List Nat) : List Nat :=
   match (xs, ys) with
@@ -21,9 +21,9 @@ def foo (xs ys zs : List Nat) : List Nat :=
 
 #eval tst ``foo
 
-#check foo._eq_1
-#check foo._eq_2
-#check foo._unfold
+#check foo.eq_1
+#check foo.eq_2
+#check foo.def
 
 #eval tst ``foo
 
@@ -35,12 +35,12 @@ 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._unfold
+#check g.eq_1
+#check g.eq_2
+#check g.eq_3
+#check g.eq_4
+#check g.eq_5
+#check g.def
 
 def h (xs : List Nat) (y : Nat) : Nat :=
   match xs with
@@ -51,9 +51,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._unfold
+#check h.eq_1
+#check h.eq_2
+#check h.def
 
 def r (i j : Nat) : Nat :=
   i +
@@ -65,10 +65,10 @@ 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._unfold
+#check r.eq_1
+#check r.eq_2
+#check r.eq_3
+#check r.def
 
 def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α :=
   f i <|
@@ -80,7 +80,7 @@ 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._unfold
+#check @bla.eq_1
+#check @bla.eq_2
+#check @bla.eq_3
+#check @bla.def
diff --git a/tests/lean/run/structuralEqns2.lean b/tests/lean/run/structuralEqns2.lean
index 4d9d9a1fac..83f8dd3791 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._unfold
+#check g.eq_1
+#check g.eq_2
+#check g.def
 
 def h (i j : Nat) : Nat :=
   let z :=
@@ -24,6 +24,6 @@ def h (i j : Nat) : Nat :=
   z + z
 
 #eval tst ``h
-#check h._eq_1
-#check h._eq_2
-#check h._unfold
+#check h.eq_1
+#check h.eq_2
+#check h.def
diff --git a/tests/lean/run/structuralEqns3.lean b/tests/lean/run/structuralEqns3.lean
index ac72ee0522..09aa049b21 100644
--- a/tests/lean/run/structuralEqns3.lean
+++ b/tests/lean/run/structuralEqns3.lean
@@ -15,6 +15,6 @@ 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._unfold
+#check @wk_comp.eq_1
+#check @wk_comp.eq_2
+#check @wk_comp.def
diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean
index 1e3e4fb768..598d1692f4 100644
--- a/tests/lean/run/wfEqns1.lean
+++ b/tests/lean/run/wfEqns1.lean
@@ -22,6 +22,6 @@ end
 #print isEven
 
 #eval tst ``isEven
-#check @isEven._eq_1
-#check @isEven._eq_2
-#check @isEven._unfold
+#check @isEven.eq_1
+#check @isEven.eq_2
+#check @isEven.def
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index aaf8670cb3..c0b5dfc117 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -31,10 +31,10 @@ decreasing_by
 end
 
 #eval tst ``g
-#check g._eq_1
-#check g._eq_2
-#check g._unfold
+#check g.eq_1
+#check g.eq_2
+#check g.def
 #eval tst ``h
-#check h._eq_1
-#check h._eq_2
-#check h._unfold
+#check h.eq_1
+#check h.eq_2
+#check h.def
diff --git a/tests/lean/run/wfEqns3.lean b/tests/lean/run/wfEqns3.lean
index 850766036e..b57d06aa4c 100644
--- a/tests/lean/run/wfEqns3.lean
+++ b/tests/lean/run/wfEqns3.lean
@@ -15,5 +15,5 @@ decreasing_by
   exact h
 
 #eval tst ``f
-#check f._eq_1
-#check f._unfold
+#check f.eq_1
+#check f.def
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index d6549693aa..7b683f879e 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -37,12 +37,12 @@ end
 #eval f 5 'a' 'b'
 
 #eval tst ``f
-#check @f._eq_1
-#check @f._eq_2
-#check @f._unfold
+#check @f.eq_1
+#check @f.eq_2
+#check @f.def
 
 
 #eval tst ``h
-#check @h._eq_1
-#check @h._eq_2
-#check @h._unfold
+#check @h.eq_1
+#check @h.eq_2
+#check @h.def
diff --git a/tests/lean/structuralEqns.lean.expected.out b/tests/lean/structuralEqns.lean.expected.out
deleted file mode 100644
index 5e1dc23bdf..0000000000
--- a/tests/lean/structuralEqns.lean.expected.out
+++ /dev/null
@@ -1,15 +0,0 @@
-(some _private.structuralEqns.0.foo._unfold)
-foo._unfold (xs ys zs : List Nat) :
-  foo xs ys zs =
-    match (xs, ys) with
-    | (xs', ys') =>
-      match zs with
-      | z :: zs => foo xs ys zs
-      | x =>
-        match ys' with
-        | [] => [1]
-        | x => [2]
-def bar : List Nat → List Nat → List Nat :=
-fun xs ys =>
-  match xs ++ [], ys ++ [] with
-  | xs', ys' => xs' ++ ys'