2022-07-16 01:42:43 +03:00
|
|
|
Bool : Type
|
|
|
|
True : Bool
|
|
|
|
False : Bool
|
|
|
|
|
|
|
|
Nat : Type
|
|
|
|
Zero : Nat
|
|
|
|
Succ (pred: Nat) : Nat
|
|
|
|
|
|
|
|
List (a: Type) : Type
|
|
|
|
Nil (a: Type) : (List a)
|
|
|
|
Cons (a: Type) (x: a) (xs: (List a)) : (List a)
|
|
|
|
|
|
|
|
Equal (t: Type) (a: t) (b: t) : Type
|
|
|
|
Refl (t: Type) (a: t) : (Equal t a a)
|
|
|
|
|
|
|
|
Bool.not (a: Bool) : Bool
|
|
|
|
Bool.not True = False
|
|
|
|
Bool.not False = True
|
|
|
|
|
|
|
|
Bool.and (a: Bool) (b: Bool) : Bool
|
|
|
|
Bool.and True True = True
|
|
|
|
Bool.and True False = False
|
|
|
|
Bool.and False True = False
|
|
|
|
Bool.and False False = False
|
|
|
|
|
2022-07-16 06:52:56 +03:00
|
|
|
Bool.theo (a: Bool) : (Equal Bool a (Bool.not (Bool.not a)))
|
|
|
|
Bool.theo a = ?a
|
|
|
|
|
|
|
|
Nat.double (x: Nat) : Nat
|
|
|
|
Nat.double (Succ x) = (Succ (Succ (Nat.double x)))
|
|
|
|
Nat.double (Zero) = (Zero)
|
|
|
|
|
2022-07-16 01:42:43 +03:00
|
|
|
List.negate (xs: (List Bool)) : (List Bool)
|
|
|
|
List.negate (Cons Bool x xs) = (Cons Bool (Bool.not x) (List.negate xs))
|
|
|
|
List.negate (Nil Bool) = (Nil Bool)
|
|
|
|
|
2022-07-16 06:52:56 +03:00
|
|
|
List.tail (a: Type) (xs: (List a)) : (List a)
|
|
|
|
List.tail a (Cons t x xs) = xs
|
|
|
|
|
2022-07-16 02:10:59 +03:00
|
|
|
List.map (a: Type) (b: Type) (x: (List a)) (f: (x: a) b) : (List b)
|
|
|
|
List.map a b (Nil t) f = (Nil b)
|
|
|
|
List.map a b (Cons t x xs) f = (Cons b (f x) (List.map a b xs f))
|
|
|
|
|
2022-07-16 01:42:43 +03:00
|
|
|
Equal.mirror (t: Type) (a: t) (b: t) (e: (Equal t a b)) : (Equal t b a)
|
|
|
|
Equal.mirror t a b (Refl u k) = (Refl u k)
|
|
|
|
|
2022-07-16 06:52:56 +03:00
|
|
|
Equal.apply (t: Type) (u: Type) (a: t) (b: t) (f: t -> t) (e: (Equal t a b)) : (Equal t (f a) (f b))
|
2022-07-16 01:42:43 +03:00
|
|
|
Equal.apply t u a b f (Refl v k) = (Refl v (f k))
|
|
|
|
|
2022-07-16 06:52:56 +03:00
|
|
|
Equal.rewrite (t: Type) (a: t) (b: t) (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
|
2022-07-16 01:42:43 +03:00
|
|
|
Equal.rewrite t a b (Refl u k) p x = {x :: (p k)}
|
|
|
|
|
|
|
|
Main : Nat {
|
2022-07-16 06:52:56 +03:00
|
|
|
let f = {(@x @y y) :: Nat -> Nat -> Nat}
|
|
|
|
(f Zero (Nat.double (Succ (Succ (Succ Zero)))))
|
2022-07-16 01:42:43 +03:00
|
|
|
}
|