dtlc

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

church.dtlc (247B)

      1 \ This is a comment.
      2 N := [A: Type, A, A -> A] -> A;
      3 add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;
      4 two: N := fn A, z, s => s (s z);
      5 three: N := fn A, z, s => s (s (s z));
      6 `f i v e` := add two three;
      7 `f i v e` Nat 0 (fn n => n + 1)