21 lines
488 B
Idris
21 lines
488 B
Idris
module HomeworkSix
|
|
%default total
|
|
|
|
data Term = Tru | Fls | Not Term | Cond Term Term Term
|
|
|
|
data OT : Term -> Type where
|
|
OptNotNot : OT (Not (Not t))
|
|
OptNot : OT t -> OT (Not t)
|
|
OptCond1 : OT t1 -> OT (Cond t1 t2 t3)
|
|
OptCond2 : OT t2 -> OT (Cond t1 t2 t3)
|
|
OptCond3 : OT t3 -> OT (Cond t1 t2 t3)
|
|
|
|
p1 : OT (Cond (Not Tru) (Not (Not Tru)) Fls)
|
|
p1 = OptCond2 OptNotNot
|
|
|
|
p2 : OT (Not (Not (Not Fls)))
|
|
p2 = OptNotNot
|
|
|
|
p3 : OT (Not (Cond (Not Tru) (Not (Not Tru)) Fls))
|
|
p3 = OptNot p1
|