From f0b2621047c72bb4985aaf8016d487576a84832b Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 29 Apr 2024 14:45:53 +0200
Subject: [PATCH] test: add guard_msgs to wfEqns tests (#4024)

otherwise we would not catch changes to the shape of these equational
lemmas.

Also, no need to manually trigger the generation of these lemmas.
---
 tests/lean/run/wfEqns1.lean | 48 +++++++++++++++++++++++++++++--------
 tests/lean/run/wfEqns2.lean | 48 ++++++++++++++++++++++++++++++-------
 tests/lean/run/wfEqns3.lean | 17 ++++++-------
 tests/lean/run/wfEqns4.lean | 45 ++++++++++++++++++++++++++--------
 tests/lean/run/wfEqns5.lean | 38 +++++++++++++++++++++++++++++
 5 files changed, 159 insertions(+), 37 deletions(-)
 create mode 100644 tests/lean/run/wfEqns5.lean

diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean
index 123b638039..b4a832465d 100644
--- a/tests/lean/run/wfEqns1.lean
+++ b/tests/lean/run/wfEqns1.lean
@@ -1,10 +1,3 @@
-import Lean
-
-open Lean
-open Lean.Meta
-def tst (declName : Name) : MetaM Unit := do
-  IO.println (← getUnfoldEqnFor? declName)
-
 mutual
   def isEven : Nat → Bool
     | 0 => true
@@ -19,9 +12,44 @@ mutual
     sorry
 end
 
-#print isEven
-
-#eval tst ``isEven
+/-- info: isEven.eq_1 : isEven 0 = true -/
+#guard_msgs in
 #check @isEven.eq_1
+/-- info: isEven.eq_2 : ∀ (n : Nat), isEven n.succ = isOdd n -/
+#guard_msgs in
 #check @isEven.eq_2
+/--
+info: isEven.eq_def : ∀ (x : Nat),
+  isEven x =
+    match x with
+    | 0 => true
+    | n.succ => isOdd n
+-/
+#guard_msgs in
 #check @isEven.eq_def
+
+/-- info: isEven.eq_2 : ∀ (n : Nat), isEven n.succ = isOdd n -/
+#guard_msgs in
+#check @isEven.eq_2
+
+/-- info: isOdd.eq_1 : isOdd 0 = false -/
+#guard_msgs in
+#check @isOdd.eq_1
+
+/-- info: isOdd.eq_2 : ∀ (n : Nat), isOdd n.succ = isEven n -/
+#guard_msgs in
+#check @isOdd.eq_2
+
+/--
+info: isOdd.eq_def : ∀ (x : Nat),
+  isOdd x =
+    match x with
+    | 0 => false
+    | n.succ => isEven n
+-/
+#guard_msgs in
+#check @isOdd.eq_def
+
+/-- info: isEven.eq_2 : ∀ (n : Nat), isEven n.succ = isOdd n -/
+#guard_msgs in
+#check @isEven.eq_2
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index 7df64d73cb..8909548bae 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -1,10 +1,3 @@
-import Lean
-
-open Lean
-open Lean.Meta
-def tst (declName : Name) : MetaM Unit := do
-  IO.println (← getUnfoldEqnFor? declName)
-
 mutual
 def g (i j : Nat) : Nat :=
   if i < 5 then 0 else
@@ -30,11 +23,48 @@ decreasing_by
     apply Nat.lt_succ_self
 end
 
-#eval tst ``g
+/-- info: g.eq_1 (i : Nat) : g i Nat.zero = if i < 5 then 0 else 1 -/
+#guard_msgs in
 #check g.eq_1
+
+/-- info: g.eq_2 (i j_2 : Nat) : g i j_2.succ = if i < 5 then 0 else h i j_2 -/
+#guard_msgs in
 #check g.eq_2
+
+/--
+info: g.eq_def (i j : Nat) :
+  g i j =
+    if i < 5 then 0
+    else
+      match j with
+      | Nat.zero => 1
+      | j.succ => h i j
+-/
+#guard_msgs in
 #check g.eq_def
-#eval tst ``h
+
+/-- error: unknown identifier 'g.eq_3' -/
+#guard_msgs in
+#check g.eq_3
+
+/-- info: h.eq_1 (i : Nat) : h i 0 = g i 0 -/
+#guard_msgs in
 #check h.eq_1
+
+/-- info: h.eq_2 (i j_2 : Nat) : h i j_2.succ = g i j_2 -/
+#guard_msgs in
 #check h.eq_2
+
+/--
+info: h.eq_def (i j : Nat) :
+  h i j =
+    match j with
+    | 0 => g i 0
+    | j.succ => g i j
+-/
+#guard_msgs in
 #check h.eq_def
+
+/-- error: unknown identifier 'h.eq_3' -/
+#guard_msgs in
+#check h.eq_3
diff --git a/tests/lean/run/wfEqns3.lean b/tests/lean/run/wfEqns3.lean
index dfdf6b6a87..bfe99b7c21 100644
--- a/tests/lean/run/wfEqns3.lean
+++ b/tests/lean/run/wfEqns3.lean
@@ -1,10 +1,3 @@
-import Lean
-
-open Lean
-open Lean.Meta
-def tst (declName : Name) : MetaM Unit := do
-  IO.println (← getUnfoldEqnFor? declName)
-
 def f (x : Nat) : Nat :=
   if h : x = 0 then
     1
@@ -14,6 +7,14 @@ decreasing_by
   apply Nat.pred_lt
   exact h
 
-#eval tst ``f
+/-- info: f.eq_1 (x : Nat) : f x = if h : x = 0 then 1 else f (x - 1) * 2 -/
+#guard_msgs in
 #check f.eq_1
+
+/-- info: f.eq_def (x : Nat) : f x = if h : x = 0 then 1 else f (x - 1) * 2 -/
+#guard_msgs in
 #check f.eq_def
+
+/-- error: unknown identifier 'f.eq_2' -/
+#guard_msgs in
+#check f.eq_2
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index d91dde41fe..9496a9ab40 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -1,10 +1,3 @@
-import Lean
-
-open Lean
-open Lean.Meta
-def tst (declName : Name) : MetaM Unit := do
-  IO.println (← getUnfoldEqnFor? declName)
-
 mutual
   def f : Nat → α → α → α
     | 0, a, b => a
@@ -34,15 +27,47 @@ mutual
     apply Nat.lt_succ_self
 end
 
+/-- info: 'a' -/
+#guard_msgs in
 #eval f 5 'a' 'b'
 
-#eval tst ``f
+/-- info: @f.eq_1 : ∀ {α : Type u_1} (x x_1 : α), f 0 x x_1 = x -/
+#guard_msgs in
 #check @f.eq_1
+/--
+info: @f.eq_2 : ∀ {α : Type u_1} (x : Nat) (x_1 x_2 : α), (x = 0 → False) → f x x_1 x_2 = (g x_1 x x_2).fst
+-/
+#guard_msgs in
 #check @f.eq_2
+/--
+info: @f.eq_def : ∀ {α : Type u_1} (x : Nat) (x_1 x_2 : α),
+  f x x_1 x_2 =
+    match x, x_1, x_2 with
+    | 0, a, b => a
+    | n, a, b => (g a n b).fst
+-/
+#guard_msgs in
 #check @f.eq_def
+/-- error: unknown identifier 'f.eq_3' -/
+#guard_msgs in
+#check @f.eq_3
 
-
-#eval tst ``h
+/-- info: @h.eq_1 : ∀ {α : Type u_1} (x x_1 : α), h x x_1 0 = x_1 -/
+#guard_msgs in
 #check @h.eq_1
+/-- info: @h.eq_2 : ∀ {α : Type u_1} (x x_1 : α) (n : Nat), h x x_1 n.succ = f n x x_1 -/
+#guard_msgs in
 #check @h.eq_2
+/--
+info: @h.eq_def : ∀ {α : Type u_1} (x x_1 : α) (x_2 : Nat),
+  h x x_1 x_2 =
+    match x, x_1, x_2 with
+    | a, b, 0 => b
+    | a, b, n.succ => f n a b
+-/
+#guard_msgs in
 #check @h.eq_def
+
+/-- error: unknown identifier 'h.eq_3' -/
+#guard_msgs in
+#check @h.eq_3
diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean
new file mode 100644
index 0000000000..6430ad3c4d
--- /dev/null
+++ b/tests/lean/run/wfEqns5.lean
@@ -0,0 +1,38 @@
+
+def foo : Nat → Nat → Nat
+  | 0, m => match m with | 0 => 0 | m => m
+  | n+1, m => foo n m
+termination_by n => n
+
+/--
+info: foo.eq_1 :
+  ∀ (x : Nat),
+    foo 0 x =
+      match x with
+      | 0 => 0
+      | m => m
+-/
+#guard_msgs in
+#check foo.eq_1
+
+/-- info: foo.eq_2 : ∀ (x n : Nat), foo n.succ x = foo n x -/
+#guard_msgs in
+#check foo.eq_2
+
+/--
+info: foo.eq_def :
+  ∀ (x x_1 : Nat),
+    foo x x_1 =
+      match x, x_1 with
+      | 0, m =>
+        match m with
+        | 0 => 0
+        | m => m
+      | n.succ, m => foo n m
+-/
+#guard_msgs in
+#check foo.eq_def
+
+/-- error: unknown identifier 'foo.eq_3' -/
+#guard_msgs in
+#check foo.eq_3