From 8689a56a5da04b70dd8ac986f48cb5bd836e3b5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 3 Mar 2024 18:32:20 -0800
Subject: [PATCH] feat: `#print equations <decl-name>` command (#3584)

---
 src/Lean/Elab/Print.lean      | 15 +++++++++++++++
 src/Lean/Parser/Command.lean  |  2 ++
 tests/lean/run/printEqns.lean | 31 +++++++++++++++++++++++++++++++
 3 files changed, 48 insertions(+)
 create mode 100644 tests/lean/run/printEqns.lean

diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index e96e50bffa..77d77a0842 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.FoldConsts
+import Lean.Meta.Eqns
 import Lean.Elab.Command
 
 namespace Lean.Elab.Command
@@ -128,4 +129,18 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax
 
+private def printEqnsOf (constName : Name) : CommandElabM Unit := do
+  let some eqns ← liftTermElabM <| Meta.getEqnsFor? constName (nonRec := true) |
+    logInfo m!"'{constName}' does not have equations"
+  let mut m := m!"equations:"
+  for eq in eqns do
+    let cinfo ← getConstInfo eq
+    m := m ++ Format.line ++ (← mkHeader "theorem" eq cinfo.levelParams cinfo.type .safe)
+  logInfo m
+
+@[builtin_command_elab «printEqns»] def elabPrintEqns : CommandElab := fun stx => do
+  let id := stx[2]
+  let cs ← resolveGlobalConstWithInfos id
+  cs.forM printEqnsOf
+
 end Lean.Elab.Command
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 6c87e15057..4363d91583 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -230,6 +230,8 @@ def «structure»          := leading_parser
   "#print " >> (ident <|> strLit)
 @[builtin_command_parser] def printAxioms    := leading_parser
   "#print " >> nonReservedSymbol "axioms " >> ident
+@[builtin_command_parser] def printEqns      := leading_parser
+  "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
diff --git a/tests/lean/run/printEqns.lean b/tests/lean/run/printEqns.lean
new file mode 100644
index 0000000000..c0a0d06c0b
--- /dev/null
+++ b/tests/lean/run/printEqns.lean
@@ -0,0 +1,31 @@
+/--
+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 α),
+  List.append (a :: l) x = a :: List.append l x
+-/
+#guard_msgs in
+#print eqns List.append
+
+/--
+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 α),
+  List.append (a :: l) x = a :: List.append l x
+-/
+#guard_msgs in
+#print equations List.append
+
+@[simp] def ack : Nat → Nat → Nat
+  | 0,   y   => y+1
+  | x+1, 0   => ack x 1
+  | x+1, y+1 => ack x (ack (x+1) y)
+
+/--
+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)
+-/
+#guard_msgs in
+#print eqns ack