--- Day changed Mon Jan 16 2017
apostolisHello, I have prf : ¬T , thus prf tt = ⊥.16/01 12:35
apostolisWhich function should I use to dismiss this patter case?16/01 12:36
apostolisIdris has the void function.16/01 12:37
{AS}apostolis: ⊥-elim16/01 12:39
apostolisok16/01 12:39
apostolisHey, {AS} , does agda dismiss impossible cases immediately? 16/01 12:41
{AS}apostolis: what do you mean?16/01 12:41
{AS}It will usually dismiss impossible cases if it finds out they are16/01 12:42
apostolisHere I have prf : \neg T and it is annoying that I have to use ⊥-elim (prf tt)16/01 12:42
{AS}if not you may have to use the void pattern ()16/01 12:42
{AS}apostolis: but it doesn't necessarily know that ¬T is impossible16/01 12:43
apostolisI know16/01 12:43
{AS}that is why you have to use ⊥-elim16/01 12:43
apostolisYes.16/01 12:43
{AS}if you had something which will lead to a unification error, you can just pattern match on it16/01 12:43
{AS}and it will use the () pattern the right place to mark it impossible16/01 12:43
apostolisOk, let me look at that.16/01 12:44
{AS}apostolis: why do you have \neg T anyway?16/01 12:46
apostolisI have a function that returns T or ⊥ named belongs.16/01 12:47
apostolisAnd I want something to not belong, thus \neg belongs.16/01 12:48
{AS}Ah16/01 12:48
apostolisI use them instead of false, true. I think that they are better.16/01 12:48
{AS}apostolis: why don't you just define not-belongs? :)16/01 12:49
apostolisYea, that came into my mind, anoying right :)16/01 12:49
drdoNow I understand why people came up with the whole tactics thing.16/01 18:28
drdoHaving to manually construct the correct sequence of swaps to show something by commutativity and associativity is no fun16/01 18:29
comietekReflection could help with that. http://www.cs.ox.ac.uk/people/ohad.kammar/s-repls-5/abstracts.html#Bradley%20Hardy16/01 19:27

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