<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 12pt;
font-family:????
}
--></style></head>
<body class='hmmessage'><div dir='ltr'><div>Hi ,</div><div><br></div><div>i googled an example and run and got error</div><div><br></div><div><div>/home/martin/hilbertreborn/LogicLib.agda:5,2: Not a valid pattern: Prop</div><div>=<ERROR></div><div> Set</div><div><br></div><div> (=>)(X,Y::Prop) :: Prop...</div></div><div><br></div><div><a href="http://ocvs.cfv.jp/Agda/tutorial/node149.html" target="_blank">http://ocvs.cfv.jp/Agda/tutorial/node149.html</a></div><div><br></div><div><br></div><div><div>/home/martin/hilbertreborn/prove2.agda:3,6-14</div><div>No such module LogicLib</div><div>when scope checking the declaration</div><div> open LogicLib use Prop, (&&) , (=>) , (<=>)</div></div><div><br></div><div><div>--#include "/home/martin/hilbertreborn/LogicLib.agda"</div><div><br></div><div>open LogicLib use Prop, (&&), (=>), (<=>) </div><div><br></div><div>prop3 (A,B,C::Prop) :: ((A && B) => C) <=> (A => (B => C))</div><div> = {}0</div></div><div><br></div><div><br></div><div>Regards,</div><div><br></div><div>Martin</div> </div></body>
</html>