language-pts-0: Pure Type Systems
language-pts
implements a pure type system, based on
A tutorial implementation of a dependently typed lambda calculus
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
- Bi-directional type-checking
bound
for terms and values (notInt
de Bruijn or HOAS)- parametrised by PTS
Specification
. - see Language.PTS module for more