- Edit examples.lean
- Uncomment lines 9 to 22 and lines 28 to 41
- Compile examples.lean using either:
- the VS code Lean tool;
- the emacs Lean tool; or
- calling
lean test/examples.lean
in a terminal
- For both
tree
andtree'
, the first line#print prefix tree
enumerates the declarations generated by Lean and by the QPF data type compiler - Below
#print prefix tree
, a list of#print
and#check
statements emphasizes the examples found in section 6 of Data types as quotients of polynomial functors