--- Day changed Tue Mar 28 2017
sleffyIs there a better way to use equational reasoning than just `open ≡-Reasoning`?28/03 06:36
{AS}sleffy: Yeah28/03 06:39
{AS}what are you trying to do?28/03 06:39
sleffyI just want to use it. I'm not using any other forms of it, so simply opening the version of it contained in `Relation.Binary.PropositionalEquality` works for me right now. But it feels clunky.28/03 06:39
sleffyAnd it obviously won't work if and when I want to use other forms of it28/03 06:40
sleffySo I guess my question is, how can I use ≡-Reasoning for propositional equality without any danger of it colliding now or later with other ≡-Reasoning modules?28/03 06:41
{AS}sleffy: you can just open it in a local anonymous module28/03 06:42
{AS}module _ where ...28/03 06:42
sleffyHow does that work with getting stuff *out* of that local anonymous module? Can I access members of it as if they're declared in the surrounding module?28/03 06:43
{AS}Yeah28/03 06:44
sleffyCool! That sounds like exactly what I'm looking for. Thanks!28/03 06:45
{AS}np28/03 06:45
Saizan{AS}: module _ where ... publicly exports all the symbols defined in ..., so i don't think that was a solution28/03 09:00
mietekSaizan: if you "open foo" inside an anonymous module, these symbols aren’t treated as defined in it28/03 09:02
mietekSaizan: as opposed to "open foo public"28/03 09:02
Saizanmietek: oh, ok28/03 09:03
Saizanmakes sense actually28/03 09:03
mietekyeah, I really like it28/03 09:03
mietekeverything about the module system in Agda rocks28/03 09:03
Saizan(and it's also a pain to implement!)28/03 09:04
Saizanor maybe the problem is that there's no fixed spec28/03 09:05
akr[m]is it usually better to define the negation of some data type as a new type, rather than simply as a negation of the original type?28/03 12:18
akr[m]I guess you can't be quite as certain that what you defined as the negation really is the same as the actual negation28/03 12:20
akr[m]hmm28/03 12:20
akr[m]no, nevermind, I don't think it makes sense to do that28/03 12:20
gallaisakr[m]: It does make sense sometimes. The main advantage is that you get *positive* proofs which you can perform induction on28/03 12:43
gallaise.g. if you're doing typechecking. Having (G |- t : A -> False) is weaker than having a derivation pointing out where exactly the impossible case is28/03 12:44
mietekwould that be called a refutation?28/03 12:44
gallaisI don't know. I usually talk about positive vs. negative evidence28/03 12:46
akr[m]Ah, interesting28/03 14:13
akr[m]Gallais: thank you28/03 14:13
glguyAnother solution to sleffy's question is to put "open ≡-Reasoning" in a where clause so that it's only opened for that definition28/03 16:20
mietek"not a legal rewrite rule, since the left-hand side is neither a defined symbol nor a constructor"28/03 16:50
akr[m]mietek: weren't you trying to avoid using rewrite precisely because of this kind of thing?28/03 17:06
akr[m]does it make life a lot easier at some point?28/03 17:07
mietekthis isn’t about `rewrite`28/03 17:07
mietekthis is about `REWRITE`28/03 17:07
akr[m]oh28/03 17:07
mietekwhat they have in common is28/03 17:07
mietekhalf the time I try to use either, it doesn’t work28/03 17:08
mietek!@#$28/03 17:08
akr[m]:D28/03 17:08
mietekI don’t even understand that error message28/03 17:08
akr[m]I still haven't even used it myself28/03 17:12

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