41 lines
1.1 KiB
Idris
41 lines
1.1 KiB
Idris
module HomeworkSixteen
|
|
|
|
%default total
|
|
|
|
data Term = T | F | Q | And Term Term
|
|
|
|
data Val : Term -> Type where
|
|
ValT : Val T
|
|
ValF : Val F
|
|
ValQ : Val Q
|
|
|
|
infixl 10 |->
|
|
data (|->) : Term -> Term -> Type where
|
|
AndFirst : (t1 |-> t1') -> (And t1 t2) |-> (And t1' t2)
|
|
AndSecond : Val t1 -> (t2 |-> t2') -> (And t1 t2) |-> (And t1 t2')
|
|
AndF : Val t2 -> And F t2 |-> F
|
|
AndT : Val t2 -> And T t2 |-> t2
|
|
AndQF : And Q F |-> F
|
|
AndQT : And Q T |-> Q
|
|
AndQQ : And Q Q |-> Q
|
|
|
|
infixl 10 |-->
|
|
data (|-->) : Term -> Term -> Type where
|
|
AndLFirst : (t1 |--> t1') -> (And t1 t2) |--> (And t1' t2)
|
|
AndLSecond : Val t1 -> (t2 |--> t2') -> (And t1 t2) |--> (And t1 t2')
|
|
AndLF : And F t2 |--> F
|
|
AndLT : And T t2 |--> t2
|
|
AndLQF : And Q F |--> F
|
|
AndLQT : And Q T |--> Q
|
|
AndLQQ : And Q Q |--> Q
|
|
|
|
infixl 10 !!
|
|
data (!!) : Term -> Term -> Type where
|
|
SemT : T !! T
|
|
SemF : F !! F
|
|
SemQ : Q !! Q
|
|
SemAndF : t1 !! F -> And t1 t2 !! F
|
|
SemAndT : t1 !! T -> t2 !! v -> And t1 t2 !! v
|
|
SemAndQF : t1 !! Q -> t2 !! F -> And t1 t2 !! F
|
|
SemAndQ : t1 !! Q -> Either (t2 !! T) (t2 !! Q) -> And t1 t2 !! Q
|