[Agda] question about instance arguments

Roly Perera roly.perera at dynamicaspects.org
Sat Dec 6 11:10:40 CET 2014


Yes, this is a great article (and helped me understand Setω, which I
only recently encountered). Thanks.

On 6 December 2014 at 08:37, Andreas Abel <abela at chalmers.se> wrote:
> Big thanks also for this article, which is a very nice tutorial on universes
> and universe polymorphism in Agda!!  --Andreas
>
> On 06.12.2014 05:41, Peter Selinger wrote:
>>
>> I also populated the article on Universe Polymorphism, which was
>> previously a stub:
>>
>>
>> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
>>
>> I hope I got it mostly right. -- Peter
>>
>> Andreas Abel wrote:
>>>
>>>
>>> Excellent!  Big thanks. --Andreas
>>>
>>> On 04.12.2014 17:45, Peter Selinger wrote:
>>>>
>>>> I've updated this page of the reference manual accordingly:
>>>>
>>>>
>>>> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments
>>>>
>>>> -- Peter
>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


More information about the Agda mailing list