<div dir="ltr">Hi all,<div><br></div><div>I&#39;m trying to figure out the basics of agda. I have a few years of haskell experience, but lack a formal maths background. However, after some trying and reading tutorials I managed to translate some proofs I found on wikipedia into agda. </div>
<div><br></div><div style>However, it&#39;s unclear to me how to use these proofs in other parts of my program, where the typechecker complains and wants some proof.</div><div style><br></div><div style>Please have a look here:</div>
<div style><a href="https://gist.github.com/bluescreen303/4947548">https://gist.github.com/bluescreen303/4947548</a><br></div><div style><br></div><div style>How do I complete these 2 definitions?</div><div style>Am I on the right track in general?</div>
<div style>Or are there easier ways to accomplish things (apart from just using the standard libraries)?</div><div style>Furthermore, I noticed I&#39;ve never used the . notation (as in suc .n), while it&#39;s quite common in other code. Probably I&#39;m doing something cumbersome to avoid them?</div>
<div style><br></div><div style>Thanks for any help,</div><div style>Mathijs</div></div>