--- Day changed Fri Jun 16 2017
quchenHow do I add another axiom (type without proof of inhabitance) into my program again?16/06 12:17
quchenSomething like »axiom: forall a. a or not a«16/06 12:17
Saizanpostulate16/06 12:18
quchenAh, thanks!16/06 12:18
quchenI was trying »proposition« and what not, but not postulate16/06 12:18
arjen-jonathanAgda seems to have more trouble with module's implicit parameters than with declaration-level implicits16/06 12:43
arjen-jonathanIs there a good reason for that?16/06 12:43
arjen-jonathanI thought the former was desugared into the latter if you open a module without specifying parameters;16/06 12:44
mietekarjen-jonathan: bugs16/06 12:50
mietekthere is never any reason for bugs16/06 12:50
mietekexcept economics16/06 12:50
arjen-jonathanmietek: but there's a difference between "to be expected bugs" and "no that really shouldn't happen bugs"16/06 13:08
arjen-jonathanMaybe I should rephrase: is my interpretation of their equivalence correct?16/06 13:08
mietektrue. I don’t know16/06 13:08
arjen-jonathanThanks for answering though :)16/06 13:09
Saizanarjen-jonathan: what kind of trouble?16/06 14:32
mietek"… is not a legal rewrite rule, since the left-hand side … reduces to …"16/06 15:50
mietekwhyyy 16/06 15:50
mietekliterally the same proof is accepted as a rewrite rule is accepted in another file16/06 15:52
mietekah. I see.16/06 15:56

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