<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:·s²Ó©úÅé
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><font size="3" style="font-size:12pt;" color="#000000">Hi ,</font><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font size="3" style="font-size:12pt;" color="#000000">when i am thinking new axiom to replace trans in Equality.agda</font></div><div><font color="#000000">((a¡÷b) ¡Ý b)¡÷((a ¡Ý a) ¡Ý c)</font></div><div>do not understand how can this replace equal, feel difficult to read standard library</div><div><br></div><div>then i start <a href="http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf" target="_blank" style="font-size: 12pt;">http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf</a></div><div><br></div><div>do not know why it do not print "it is true"</div><div><font size="3" style="font-size:12pt;" color="#000000"><br></font></div><div><font color="#000000"><div>open import Prelude</div><div><br></div><div>data Bool : Set where</div><div> true : Bool</div><div> false : Bool</div><div><br></div><div>not : Bool -> Bool</div><div>not true = false</div><div>not false = true</div><div><br></div><div>data Nat : Set where</div><div> zero : Nat</div><div> suc : Nat -> Nat</div><div><br></div><div>_+_ : Nat -> Nat -> Nat</div><div>zero * m = zero</div><div>suc n + m = suc (n + m)</div><div><br></div><div>_*_ : Nat -> Nat -> Nat</div><div>zero * m = zero</div><div>suc n * m = m + n * m</div><div><br></div><div>_or_ : Bool -> Bool -> Bool</div><div>false or x = x</div><div>true or _ = true</div><div><br></div><div>if_then_else_ : (A : Set) -> Bool -> A -> A -> A</div><div>if true then x else y = x</div><div>if false then x else y = y</div><div><br></div><div>main = </div><div> if true then putStrLn "it is true" else putStrLn "it is else case"</div><div> putStrLn "Hello World"</div></font><br><br><div>Regards,</div><div><br></div><div>Martin </div></div> </div></body>
</html>