-- a mini prelude module Stuff public export data Bool = True | False public export not : Bool -> Bool not True = False not False = True public export data Maybe : Type -> Type where Nothing : Maybe a Just : (1 x : a) -> Maybe a public export data Either : Type -> Type -> Type where Left : (1 x : a) -> Either a b Right : (1 y : b) -> Either a b public export intToBool : Int -> Bool intToBool 0 = False intToBool x = True public export ifThenElse : Bool -> Lazy a -> Lazy a -> a ifThenElse True t e = t ifThenElse False t e = e public export data Nat : Type where Z : Nat S : (1 _ : Nat) -> Nat public export fromInteger : Integer -> Nat fromInteger x = ifThenElse (intToBool (prim__eq_Integer x 0)) Z (S (fromInteger (prim__sub_Integer x 1))) public export plus : Nat -> Nat -> Nat plus Z y = y plus (S k) y = S (plus k y) infixr 5 :: public export data List : Type -> Type where Nil : List a (::) : (1 _ : a) -> (1 _ : List a) -> List a public export data Eq : a -> b -> Type where Refl : (x : a) -> Eq x x public export data Unit = MkUnit public export data Pair : Type -> Type -> Type where MkPair : {a, b : Type} -> a -> b -> Pair a b public export the : (a : Type) -> a -> a the _ x = x