--- Day changed Fri Jun 23 2017
rntzis there a way to re-export a module you've imported in agda?23/06 00:20
rntzmodule A: "import Relation.Binary.PropositionalEquality as Eq; <something here>" and then module B: "open import A; <a module named Eq is visible here>"23/06 00:21
doliorntz: open ... public23/06 03:30
Taneb"Cannot resolve overloaded projection Mor because principle argument is not of record type"23/06 07:49
Taneb:(23/06 07:49
TanebI... I think I've got a definition of functor equality23/06 07:55
TanebIt's taking a while to check this, I think I should split it into different files23/06 10:14
mietekTaneb: that error sounds like a typo23/06 20:08

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!