/home/laney/.irssi/irclogs/Freenode/#agda.log-20170124

--- Day changed Mon Jan 23 2017
byorgeyrgrinberg: you mean like \oplus or \otimes ?23/01 02:33
byorgeyyou can also type \o+ or \ox23/01 02:34
byorgeyrgrinberg: also, pro tip: if you already have a particular symbol somewhere in a buffer, put the cursor on it and C-u C-x =  will show you how to enter it23/01 02:35
subttleHi, my code is causing an internal error in Agda but I'm hesitent to file a bug report because I'm still learning and my code is pretty terrible :D The error is:23/01 09:35
subttleAn internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/Auto/CaseSplit.hs:28523/01 09:35
subttleI haven't been able to abstract the bug into a simpler case, so I was hoping someone could look at the code and help me do that so I don't have to publicly post my awful code in the bug report :D23/01 09:37
Saizan_subttle: are you using auto?23/01 09:39
Saizan_*agsy23/01 09:39
subttleSaizan_: The bug happens when I try to lookup a solution from within a hole23/01 09:40
subttleusing Ctrl-C Ctrl-A23/01 09:40
subttlehere is the code23/01 09:45
subttlehttp://pastebin.com/Ve3q4PhU23/01 09:45
subttlethe hole is on Line 18723/01 09:46
subttleif that means it is with agsy then would I report the bug somewhere else?23/01 09:50
Saizan_you would still report the bug to agda23/01 09:53
subttleOh and I'm using Agda 2.5.1 for the record23/01 09:54
subttleSaizan_: roger23/01 09:54
Saizan_subttle: from the code at  src/full/Agda/Auto/CaseSplit.hs the bug is related to metavariables, but it's hard to be more precise than that23/01 10:11
Saizan_subttle: your code is fine enough, maybe you can remove lots of the cases though?23/01 10:12
subttleSaizan_: Okay thanks. I was hoping to compact it into fewer cases once I figured out how to finish the proof first. It's taking me a while to figure out though :)23/01 10:17
Saizan_subttle: i meant just for the bug report, to make it smaller, you could delete some of the constructors from the datatypes and also cases in the functions23/01 10:19
subttleSaizan_: Ah, I see what you mean, I deleted over a thousand lines to get it this small, I should continue to trim it though :D23/01 10:21
subttleThanks for your help23/01 10:21
Saizan_cheers23/01 10:23
SuprDewdAssuming the type of x can be inferred, is there any difference between 1) ∀ x, 2) ∀ (x : T) and 3) (x : T) ?23/01 13:23
apostolisIs it possible to prove that A -> \bot , the negation of a proof is equal to any other negation of that proof.23/01 13:54
apostolis?23/01 13:54
{AS}apostolis: you need functional extensionality for that I think23/01 13:55
apostolisyes, but there must be a way to avoid it.23/01 13:55
apostolisI hope.23/01 13:56
{AS}apostolis: do you have the function in applied form?23/01 13:56
{AS}I think you can prove (x, y : \bot) -> x \== y23/01 13:56
{AS}apostolis: Yeah, you cna23/01 13:57
{AS}apostolis: Yeah, you can23/01 13:57
apostolisok, but the negation of a proof is used unapplied when we put them in constructors or in types.23/01 13:58
{AS}apostolis: why don't you just make them proof irrelevant?23/01 13:58
apostolisWhat do you mean?23/01 13:59
{AS}apostolis: like in the constructor23/01 13:59
{AS}you can just make the argument proof irrelevant23/01 13:59
apostolisI do not know what you mean? Can we do it?23/01 14:00
{AS}apostolis: I am unsure what you mean :)23/01 14:00
apostolisThe last days I was proving that my proofs are unique (any two proofs are equal).23/01 14:00
{AS}you can make Foo : .(P -> \bot) -> Bar23/01 14:01
{AS}no?23/01 14:01
apostolisThat is the standard method of putting a negation (\neg)23/01 14:02
apostolisIt just happenned to have two negations and proofs that rely on any of the two, and I can not values that have one negation with values that have the other.23/01 14:05
apostolisConsider a function f : A -> \neg C -> B23/01 14:13
apostolisRegardless of the function g : \neg C , function f will produce the same result.23/01 14:13
apostolisso one needs to prove that for g1 , g2    f a g1 = f a g2 .23/01 14:15
apostolisBut we shouldn't have to prove that. Negations should always be considered unique.23/01 14:16
{AS}apostolis: you can just postulate uniqueness :)23/01 14:18
{AS}or make the argument proof irrelevant23/01 14:19
apostolis{AS} First time postulating something. This is it.23/01 14:21
apostolis{AS} is there documentation on proof irrelevance. You must be saying something important and me not getting it.23/01 14:28
{AS}http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Irrelevance23/01 14:28
apostolis{AS} If you use a proof to eliminate a case, it cannot be irrelevant. (with \bot-elim for example)23/01 14:51
apostolisMaybe I need to make an issue to disregard \bot-elim from irrelevance checking.23/01 14:54
{AS}apostolis: you can make an irrelevant \bot-elim23/01 14:54
{AS}apostolis: I tried doing that23/01 14:54
{AS}I have a PR for the agda-stdlib23/01 14:54
apostolisOh nice.23/01 14:54
{AS}https://github.com/agda/agda-stdlib/pull/11623/01 14:55
mpickeringWhat does (f  . _::_ _) mean?23/01 15:10
mpickeringthe answer is (λ E x → θ ( _ ∷ E ) x) 23/01 15:15
mpickeringthanks!23/01 15:15
apostolis{AS} If only I knew proof irrelevance yesterday, thanks, now it works.23/01 15:42
SuprDewdis it possible to have multiple rewrites in sequence?23/01 21:14
{AS}SuprDewd: It is23/01 21:27
{AS}use |23/01 21:27
{AS}so rewrite a | b | c23/01 21:28
SuprDewd{AS}: works great, thanks!23/01 21:43
{AS}sure :)23/01 21:43

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