Print equations related to a definition

Stream: lean4

[Bhavik Mehta]

Here's my example:

import Batteries.Tactic.PrintPrefix

def myDef : Nat → Nat := fun x ↦ x + 1

I'd like to see which equational lemmas Lean generates for this definition. Here's what I tried:

#print prefix myDef
#print prefix +internals myDef
#print eqns myDef
#print equations myDef
#print myDef

but none of these told me about myDef.eq_def. How can I see the _full_ list of declarations with a given prefix, without things like this being hidden?

[Eric Wieser]

whatsnew in might do what you want here

[Bhavik Mehta]

It doesn't, it just outputs a subset of the above.

[Aaron Liu]

Note that myDef.eq_def is generated on first use, and then cached. If you don't have anything that uses myDef.eq_def then it doesn't exist.

[Bhavik Mehta]

Can you explain this some more? #check myDef.eq_def seems to tell me it exists before I use it. Or are you saying that me typing this in is using it? Even after that check, all the above don't show me this lemma

[Eric Wieser]

import Batteries.Tactic.PrintPrefix

def myDef : Nat → Nat := fun x ↦ x + 1

-- #print myDef.eq_def -- uncomment for magic
-- def foo := myDef.eq_def -- uncomment for magic

#print prefix myDef

[Eric Wieser]

Weirdly, #check has no side effect but #print does

[Aaron Liu]

#check erases its side effects

[Eric Wieser]

In that case I'm surprised that #print does not

[Bhavik Mehta]

Okay, that makes sense. But this is still pretty weird right, why do we have lemmas which behave like this: it doesn't exist until I use it, and then it does exist

[Aaron Liu]

What if you have this huge function, like docs#Lean.Meta.kabstract, but never unfold it in a proof? Then it would be a waste to have the equational lemma.

[Bhavik Mehta]

Hmm, okay

[Bhavik Mehta]

One more surprise (to me): if I use myDef.eq_unfold and don't use myDef.eq_def, then Lean also generates the eq_def lemma. (This is documented in docs#Lean.Meta.getConstUnfoldEqnFor?)

[Aaron Liu]

Also see #new members > ✔ Can I know exactly what collaterals are added by commands?