<font color="#330099"><div><font class="Apple-style-span" color="#000000">Thanks everyone for all the great tips and pointers.</font></div><div><font color="#330099"><br></font></div><div><font color="#330099"><br></font></div>
What is wrong with C-c C-n?</font><br><br>Thanks for the tip. Didn't know that one.<div><br></div><div><span style="font-family:arial, sans-serif;font-size:13px;border-collapse:collapse"><font color="#330099"><span style="border-collapse:separate;font-family:arial;font-size:small"> </span>agda -I</font></span></div>
<div><font face="arial, sans-serif"><span style="border-collapse:collapse"><br></span></font></div><div><font face="arial, sans-serif"><span style="border-collapse:collapse">Now I feel at home again.<br>
</span></font><br><font color="#330099"> I don't have this problem. I am using Aquamacs.</font><br><br>Tried Aquamacs but I still got the same problem. ⟨ and ⟩ don't show up correctly. Anyone can recommend a good font?<br>
<br><font color="#330099"> 8. How do you use {! !}? After running C-x C-l I receive suggestions<br>but can I somehow automatically insert them?</font><br>
<br>I was under the impression that {! !} should find possible solutions and let me insert them but maybe I've misunderstood the feature?<br><br><font color="#330099"> As one rarely needs products in Haskell, one rarely uses Sigma types in Agda.</font><br>
<br>Thanks. After reading about [<a href="http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory" target="_blank">http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory</a>] it became much clearer.<br><br></div><div><font color="#330099"> There is no way to define False using records.</font><br>
<br>Why not? Something to do with type theory (from now on I'll just refer to type theory whenever I don't understand something :) )? If defining True using record is such a good idea why isn't defining False using record a good idea? </div>
<div>
<br><font color="#330099"> 18. Why is the type declaration for apply (in the paper/tutorial by Ulf Norell):<br>(A : Set)(B : A -> Set) -> ((x : A) -> B x) -> (a : A) -> B a</font><br>
<br>I think I understand this one now. It's saying that the variable x will be eaten at "B x" and the variable a will be eaten at "B a" right?<br><br><font color="#330099"> You only dot if you repeat variables.</font><br>
<br></div><div>It finally became clear (I think).<br><div><br></div><div><span style="font-family:arial, sans-serif;font-size:13px;border-collapse:collapse"><div>
<font color="#330099"><span style="border-collapse:separate;font-family:arial;font-size:small"> </span>If you can use parameters this is usually better (certainly saves quantifying over them in the constructor type).</font></div>
<div><font color="#330099">But if you use the type at different instance this is not possible.</font></div>
<div><font color="#330099"><br></font></div><div>OK. Makes sense. I'll just remember to think of GADTs.</div><div><br></div><div><div><font color="#330099"><span style="border-collapse:separate;font-family:arial;font-size:small"> </span>Yes, use mutual then indent. All the definitions then can be mutual recursive.</font></div>
</div><div><br></div><div>And now I see it (mutual) all over the place. Didn't occur to me.</div><div><br></div><div><span style="white-space:pre-wrap"><font color="#330099"><span style="border-collapse:separate;font-family:arial;white-space:normal;font-size:small"> </span><a href="http://www.cs.nott.ac.uk/~txa/g53cfr/" target="_blank">http://www.cs.nott.ac.uk/~txa/g53cfr/</a></font></span></div>
<div><br></div><div>Good material, even though the difficulty increase between lecture 4 and 5 is a bit staggering.</div><div><br></div><div><br></div><div><font color="#330099"><span style="border-collapse:separate;font-family:arial;font-size:small"> </span>Nat has type Set which has type Set1 which has type Set2 and so on. We<br>
used to define multiple versions of everything,</font></div><div><font color="#330099"><span style="color:rgb(0, 0, 0)"><br></span></font></div><div><font color="#330099"><span style="color:rgb(0, 0, 0)">I can see why this is useful.</span></font></div>
<div><font color="#330099"><span style="color:rgb(0, 0, 0)"><br></span></font></div><div><font color="#330099"><span style="color:rgb(0, 0, 0)"><br></span></font></div><div><font class="Apple-style-span" color="#330099"> How can I interface between Haskell primitives (Integer, Float) and<br>
Agda primitives?</font></div><div><font class="Apple-style-span" color="#330099"><br></font></div><div><font class="Apple-style-span" color="#330099"> <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ForeignFunctionInterface" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ForeignFunctionInterface</a></font>
</div><div><font color="#330099"><br></font></div><div>So I can use variables of type Integer, Float etc using "postulate" but if I understand it correctly it's still impossible for me to express Integer and Float-values in Agda (unless I first define some Haskell variables with known integer-values, such as i1, i10, i100 etc that I map to Agda variables and then construct new integers adding these predefined values, like: i13 = i8 + i4 + i1).</div>
<div>From there it should be trivial to match Haskell IntegerS to Nat.</div><div>Am I on the right track here?</div><div><br></div><div>-- Oscar</div></span></div></div>