dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE

README (435B)

      1 Dependently-typed lambda calculus with Type-in-Type, general (mutual)
      2 recursive let bindings, (non-recursive) data types and pattern matching, and
      3 a built-in Nat type with some arthimetic and comparison operations
      4 
      5 This project is somewhat incomplete: implicit arguments are only half
      6 implemented, dependent pattern matching is broken, pattern matching
      7 on built-in Nats is not implemented.
      8 
      9 See the examples in the examples directory.