Torturing rustc by Emulating HKTs, Causing an Inductive Cycle and Borking the Compiler

ah I actually understand what coinduction is now!! thank you author for taking the time to explain it in grounded terms, very fun article lol

I think the author may Enjoy Chlipala’s book “Certified Programming with Dependant Types” it has a section on Coinductie data types. It’s written in Coq though which seems to no longer be a very cool language ;).

adam.chlipala.net/cpdt/cpdt.pdf