--- Day changed Sun Jan 22 2017 | ||

glguy | Is 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 |

glguy | To be specific: module M (_+_ : SomeType) where | 22/01 04:49 |

glguy | It 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 module | 22/01 04:53 |

rgrinberg | mietek: thanks | 22/01 07:53 |

apostolis | I 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 |

apostolis | I 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_Munteanu | apostolis, generally, the uniqueness of proofs is a property of the type system. It may be difficult to prove otherwise. | 22/01 14:34 |

Eduard_Munteanu | Coq certainly has it, but I'm unsure about Agda. | 22/01 14:35 |

Eduard_Munteanu | Because in Agda propositions and data are mixed into the same type. | 22/01 14:36 |

apostolis | What I mean is that there is equality between any two proofs, not that there is only one. | 22/01 14:38 |

apostolis | It seems that this is what you implied, ? | 22/01 14:38 |

Eduard_Munteanu | Yes. | 22/01 14:39 |

Eduard_Munteanu | Clearly, it doesn't hold for arbitrary propositions in Agda, such as x : Bool. | 22/01 14:40 |

apostolis | Yes. | 22/01 14:40 |

apostolis | I 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 |

apostolis | Thus I cannot use some information from outside. | 22/01 14:44 |

Eduard_Munteanu | If 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 |

apostolis | Yes, this is the standard propositional equality. | 22/01 14:51 |

rgrinberg | Is there a way to ask agda for the type of some expression? (after loading the module) | 22/01 20:57 |

Taneb | C-c C-d in emacs, iirc | 22/01 21:05 |

rgrinberg | Taneb: 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 |

Taneb | rgrinberg, you can do it in a {! !} thingy | 22/01 21:07 |

Taneb | (I don't know a lot of the vocabulary) | 22/01 21:08 |

Taneb | And it takes the contents of the braces hole thing | 22/01 21:08 |

rgrinberg | How 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!