feat: #print equations <decl-name> command (#3584)

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

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

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