- 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.leanin a terminal
- For both
treeandtree', the first line#print prefix treeenumerates the declarations generated by Lean and by the QPF data type compiler - Below
#print prefix tree, a list of#printand#checkstatements emphasizes the examples found in section 6 of Data types as quotients of polynomial functors
test
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||