dtlc

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

builtin.ml (230B)

      1 (* See also std.ml. *)
      2 
      3 type builtin =
      4 | Type
      5 | NatType
      6 | NatOpAdd
      7 | NatOpSub (* n < m  =>  n - m = 0 *)
      8 | NatOpMul
      9 | NatOpDiv (* n / 0 = 0 *)
     10 | NatOpMod (* n % 0 = 0 *)
     11 | NatOpLt
     12 | NatOpLe
     13 | NatOpEq
     14 | NatOpGe
     15 | NatOpGt
     16 | NatOpNe