[Agda] [agda2] how to programming the basic

[Mandy Martino]

Hi  ,
when  i  am  thinking  new  axiom to  replace  trans  in  Equality.agda((a¡÷b) ¡Ý b)¡÷((a ¡Ý a) ¡Ý c)do   not  understand  how  can  this  replace  equal,  feel  difficult to  read  standard  library
then  i  start  http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
do not  know why  it  do not  print  "it  is  true"
open import Prelude
data Bool : Set where true : Bool false : Bool
not : Bool -> Boolnot true = falsenot false = true
data Nat : Set where zero : Nat suc : Nat -> Nat
_+_ : Nat -> Nat -> Natzero * m = zerosuc n + m = suc (n + m)
_*_ : Nat -> Nat -> Natzero * m = zerosuc n * m = m + n * m
_or_ : Bool -> Bool -> Boolfalse or x = xtrue or _ = true
if_then_else_ : (A : Set) -> Bool -> A -> A -> Aif true then x else y = xif false then x else y = y
main =  if true then putStrLn "it is true" else putStrLn "it is else case" putStrLn "Hello World"

Regards,
Martin  		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160122/a76e9e3a/attachment.html