1. _tactics
  2. Dependently Typed Lambda Calculus

Commits

maloneymr  committed 37a2cb5

Add Eq, Refl to constants

  • Participants
  • Parent commits 3204e89
  • Branches default

Comments (0)

Files changed (1)

File DTLC.hs

View file
             Forall (Forall (Const "Nat") $ 
                 Forall (App (Var 2) (Var 0)) (App (Var 3) (App (Const "Succ") (Var 1)))) $
             Forall (Const "Nat") (App (Var 3) (Var 0))
-
+cTy "Eq" = (Forall (Star 0) (Forall (Var 0) 
+                               (Forall (Var 1) (Star 0)) ))
+cTy "Refl" = Forall (Star 0) (Forall (Var 0) (Const "Eq" `App` Var 1 `App` Var 0 `App` Var 0))
+cTy _ = error "Undefined constant"
 
 ty :: Term -> Term    
 ty = ty' []