Since this page seemed to get attention: I noticed elsewhere that you're apparently not supposed to export .Core modules directly; is there a better place to get equality and refl than Relation.Binary.Core?

Yes, Relation.Binary.PropositionalEquality. Please direct questions to the Agda mailing list, where you are more likely to receive a response.

Page last modified on April 22, 2009, at 05:08 PM
Powered by PmWiki