[Agda] Alectryon - My first case of Coq envy

Martin Escardo m.escardo at cs.bham.ac.uk
Thu Mar 25 22:46:53 CET 2021



On 25/03/2021 17:52, Andrew Pitts wrote:
> Alectryon! So a fundamental problem with getting something similar for
> Agda is that, as far as I know, there is no Norse god tasked with the
> care of chickens. :-)

Are you sure? Perhaps Gullinkambi would do the job.

Martin


> 
> On Thu, 25 Mar 2021 at 16:28, Carette, Jacques <carette at mcmaster.ca> wrote:
>>
>> https://plv.csail.mit.edu/blog/alectryon.html
>>
>>
>>
>> It doesn’t really get nice enough for envy until the uses of MathJAX for the Gauss lemma, and the graphics for Conway’s game of life.
>>
>>
>>
>> Jacques
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe


More information about the Agda mailing list