mini-pion

Minimalist reimplementation of pion

Features

dependent lambda calculus
- local variables
- integer and boolean literals
- let expressions
- fun expressions
- forall expressions
- function application expressions
- propositional equality
- type universes
unification
- inferring types of unnanotated parameters
- hole expressions
- implicit arguments
  - specialization
  - generalization
- pruning
recursion
- fix
- let rec
  - single recursive value binding
  - mutually recursive value bindings
- termination checking
aggregate types
- dependent pairs
- record types
- sum types
- row types
pattern matching
- if expressions
  - dependent if expressions
- single-layer pattern matching over integers and booleans
- multi-layer pattern matching compilation w/ coverage checking
- or-patterns
- and-patterns
- as-patterns
- pattern guards
user interface
- pion check
- pion repl
- pion fmt
- "commands" a la Lean4/Rocq (eg #check term, #print metavars)
documentation
- code comments
- tutorial
- typing rules
- bibliography
- spec