<div dir="ltr"><div>I agree with Nils points, <br><br></div><div>i think that it is better to return an error if you try to generalize a name that already exists.<br><br></div><div>In idris, where every implicit argument is generalized, you get into problems because of that.<br></div><div>You want your function to get a specific value, but instead it assumes that it is an implicit argument.<br><br><a href="http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#using-notation">http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#using-notation</a> <br></div><div>(Check the "important section" there)<br><br></div><div>So, if it returns an error in such a case and since generalization are local, this might work.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 29, 2018 at 8:39 PM, Robby Findler <span dir="ltr"><<a href="mailto:robby@eecs.northwestern.edu" target="_blank">robby@eecs.northwestern.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Thu, Mar 29, 2018 at 12:24 PM, Thorsten Altenkirch<br>
<<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@<wbr>nottingham.ac.uk</a>> wrote:<br>
> I like it too. Also one wouldn't need to doctor agda code anymore to make it publishable (destroying the literate idea in the process).<br>
<br>
</span>Yay! "Run your research" support in Agda! I love it.<br>
<br>
More generally, while I'm a total newbie compared to most people here,<br>
I really do love the design of Agda. It is so ... I don't have a good<br>
word for it ... *human*. I love the idea that it gets features that<br>
make it easier to show sensible and yet accurate code snippets in<br>
papers.<br>
<span class="HOEnZb"><font color="#888888"><br>
Robby<br>
</font></span><div class="HOEnZb"><div class="h5">______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>