[Agda] Verifying type inference in Agda?

[Peter Thiemann]

IIRC Kenichi Asai has looked into that based on Conor's unification algorithm.

-Peter


> On 29. Sep 2020, at 23:40, William Harrison <william.lawrence.harrison at gmail.com> wrote:
> 
> Hi,
> 
> I’m wondering if anyone has a pointer to a case study of verifying a type inference algorithm in Agda? Simple examples (even a toy example) would be alright (even preferred). I’m mainly interested in the structuring of the verifications in Agda.
> 
> Thanks,
> Bill
> 
> Sent from my iPad
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda