rust implementation for a subset of the agda programming language1
- indexed families of data types
- definitions by dependent pattern matching
- implicit arguments
- holes
- granular caching
crates/ -- rust code
├─ miniagda/ -- the actual language implementation
├─ miniagda-bin/ -- standalone binary elaborate an agda file once with debugging options
└─ miniagda-watch/ -- standalone binary with tui to actively work on an agda file
examples/ -- example agda files that can be elaborated using miniagda
materials/ -- presentation slides
scripts/ -- development and installation scripts
- J. Cockx: Dependent pattern matching and proof-relevant unification
- J. Cockx, A. Abel: Elaborating dependent (co)pattern matching
- A. Kovacs: Elaboration with first-class implicit function types
- A. Abel, B. Pientka: Higher-Order Dynamic Pattern Unification for Dependent Types and Records
Footnotes
-
masters project at the chair of programming languages @ uni freiburg ↩