Commits

Anonymous committed abf1d09

whoops

  • Participants
  • Parent commits 77a6477

Comments (0)

Files changed (1)

agda/helloworld.lagda

-module AgdaBasics where
-
-data Bool : Set where 
-  true : Bool
-  false : Bool
-
-not : Bool -> Bool
-not true = false
-not false = true
-
-data Nat : Set where
-  zero : Nat
-  succ : Nat -> Nat
-
-_+_ : Nat -> Nat -> Nat
-zero + m = m
-succ n + m = succ (n + m)
-
-_*_ : Nat -> Nat -> Nat
-zero * m = zero
-succ n * m = m + n * m
-
-_or_ : Bool -> Bool -> Bool
-true or x = x
-false or _ = false
-
-data List (A : Set) : Set where
-  [] : List A
-  _::_  : A -> List A -> List A
-
-identity : (A : Set) -> A -> A
-identity A x = x
-
-zero' : Nat
-zero' = identity Nat zero