Skip to content

Latest commit

 

History

History
11 lines (9 loc) · 609 Bytes

README.md

File metadata and controls

11 lines (9 loc) · 609 Bytes
Raw

Testing the Data Type Compiler

  1. Edit examples.lean
  2. Uncomment lines 9 to 22 and lines 28 to 41
  3. Compile examples.lean using either:
    • the VS code Lean tool;
    • the emacs Lean tool; or
    • calling lean test/examples.lean in a terminal
  4. For both tree and tree', the first line #print prefix tree enumerates the declarations generated by Lean and by the QPF data type compiler
  5. 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