--- Day changed Sun Jan 22 2017
glguyIs it still the case that I can't specify a fixity for a module parameter?22/01 04:49
glguy(I've been out of the loop for a bit)22/01 04:49
glguyTo be specific: module M (_+_ : SomeType) where22/01 04:49
glguyIt occurs to me that I can take a value of a record as a parameter which has a binary operator as a field, and then open that inside my module22/01 04:53
rgrinbergmietek: thanks22/01 07:53
apostolisI am in the position that I have to prove that a predicate is unique with respect to the values it depends. Is this a common pattern?22/01 14:26
apostolisI don't know if I assume the term predicate correctly, I want to show that there is only one proof for a specific type.22/01 14:31
Eduard_Munteanuapostolis, generally, the uniqueness of proofs is a property of the type system. It may be difficult to prove otherwise.22/01 14:34
Eduard_MunteanuCoq certainly has it, but I'm unsure about Agda.22/01 14:35
Eduard_MunteanuBecause in Agda propositions and data are mixed into the same type.22/01 14:36
apostolisWhat I mean is that there is equality between any two proofs, not that there is only one.22/01 14:38
apostolisIt seems that this is what you implied, ?22/01 14:38
Eduard_MunteanuYes.22/01 14:39
Eduard_MunteanuClearly, it doesn't hold for arbitrary propositions in Agda, such as x : Bool.22/01 14:40
apostolisYes.22/01 14:40
apostolisI have a proof for type B , but when I want to prove a \neg A , one constructor contains a possibly different instance of the proof B.22/01 14:44
apostolisThus I cannot use some information from outside.22/01 14:44
Eduard_MunteanuIf B is an identity proof then it can only be refl, I think.22/01 14:47
Eduard_Munteanu(in that case, pattern-match it)22/01 14:47
apostolisYes, this is the standard propositional equality.22/01 14:51
rgrinbergIs there a way to ask agda for the type of some expression? (after loading the module)22/01 20:57
TanebC-c C-d in emacs, iirc22/01 21:05
rgrinbergTaneb: I see. Although that doesn't work for selections and I'm unable to input math symbols in the minibuffer prompt :/22/01 21:07
Tanebrgrinberg, you can do it in a {! !} thingy22/01 21:07
Taneb(I don't know a lot of the vocabulary)22/01 21:08
TanebAnd it takes the contents of the braces hole thing22/01 21:08
rgrinbergHow do I input a tensor product/sum in agda? Sorry, this is hard to google -_-22/01 21:34

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