How does one print and expand everything in a Coq term (e.g. implicits, notations, definition, everything)? I want to print absolutely everything (including the contents of the identifiers).
For example with a term, I tried a modest example with Set Printing All. but it didn't work as I expect. My script is:
Module print_everything.
Definition id {A:Type} (x:A) := x.
Print id.
Definition id2 := @id.
Print id2.
Set Printing All.
Print id2.
Print All.
End.
but when I sent it to coq I got:
id2 = @id
: forall (A : Type) (_ : A), A
but I expect the body of the function, something like this:
id2 = fun (A : Type) (x : A) => x
: forall (A : Type) (_ : A), A
or
id = fun (A : Type) (x : A) => x
: forall (A : Type) (_ : A), A
How does one remove all "abstractions", including notation, implicit and even identifiers
so that I can see the entire lambda term (ideally when passing a Gallina term to Print_everything)?
If possible I'd like to control the scopes of which definitions are unpacked for me too. e.g. global variables qualid . qualid.
How does one print and expand everything in a Coq term (e.g. implicits, notations, definition, everything)?
It would also be nice to be able to expand and simplify as much as possible.
Related:
- How to temporarily disable notations in Coq
- https://coq.discourse.group/t/how-to-unset-printing-everything-e-g-implicits-notations-etc/1364/4
- it seems
Show Proof.works in the middle of a proof: https://www.seas.upenn.edu/~cis500/cis500-f14/sf/ProofObjects.html and https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html