QoC

Plan

• (Jan 5): Begin working on normalization+type checking, parser+printer.

Papers

• Lean pratt parser notes
• The foil
• Miller's pattern unification
• eliminating-dependent-pattern-matching
• universe-levels-via-displacement-algebras
• elaboration-in-dependent-type-theory
• anti-unification
• pattern matching without k

Installation

• Execute ghcup
• Clone repo
• Run stack build
• stack exec qoc to execute, stack ghci for REPL.
• Send a proven correct and yet incorrect implementation!