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