--- Day changed Mon Jan 22 2018
pgiarrussoIIRC irrelevance affects what you can prove... (irrelevant proofs of the same goal are equal)... speculation: “runtime irrelevant” argument doesn’t affect what you can prove but only the runtime behavior (that is, those arguments are erased?)22/01 00:21
pgiarrussoanyway, worst-case I‘d take the `master` branch and bisect Agda till the prelude breaks to find info22/01 00:22
pgiarrussoor check which branch the prelude is supposed to work with22/01 00:22
pgiarrussotrikl[m]: looking at the source leads to https://github.com/agda/agda/issues/2757 and McBride’s “plenty of nutting” (https://github.com/agda/agda/commit/581cc7a8d74bcf29e7bd2e43e84a97fd65bbc860)22/01 00:26
pgiarrussotrikl[m]: but the issue is open and not obvious, so I don’t think the feature is really ready for us end-users22/01 00:28
pgiarrussoOTOH Ulf Norell is a different matter22/01 00:28
trikl[m]At least now I know I can safely ignore it :)22/01 00:30
trikl[m]Thanks pgiarrusso :)22/01 00:30
pgiarrusso:-)22/01 00:36

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