--- Day changed Wed Aug 09 2017 | ||

carter | Dolio: byorgey : the changelog entry explaining the exact split flag actually talks about this curly | 09/08 02:25 |
---|---|---|

carter | Nicely | 09/08 02:25 |

carter | Default agda semantic when there's overlap is to pick the first match, as long as the matches don't unify as equal. With exact split , it rejects overlapping equations in pattern matching because their reductions as case trees don't line up with the reductions that the defining pattern equations induce | 09/08 02:28 |

carter | I think nonderermistic rewrite systems or backtracking stuff can let you have those ... but agda isn't that afaict | 09/08 02:28 |

carter | :) | 09/08 02:28 |

kclancy | Noob question. For an Agda project I am working on, I need a way to reason about sets of variables. Specifically, the set of variables in a typing context. Agda's standard library has Data.AVL.Sets, but it does not seem to provide any theorems about sets. For example, I would like a theorem stating that for all v, v \in (insert s v). Should I just my own Set library? (I would use lists rather than AVL trees, since I don't need computational efficiency.) | 09/08 18:51 |

kclancy | My impression is that Agda does not have very developed libraries, and that it is probably just easier in many cases to write one's own libraries. | 09/08 18:52 |

kclancy | I doubt this caused any confusion, but just to clarify: by (insert s v) in the above description, I meant inserting a value v into a set s. | 09/08 18:54 |

Saizan_ | dolio: in Conor's system you had "|- (\x. x) :0 (x :0 A) -> A" which i wouldn't call parametric, i would have to look at atkey's more closely though | 09/08 19:08 |

dolio | Oh, really? | 09/08 19:09 |

Saizan_ | yeah, because the typing rule for lambda goes like this "G |- (\x. t) :r (x :p A) -> B" <== "G , x :pr A |- t :r B" | 09/08 19:13 |

dolio | Yeah, I see. | 09/08 19:22 |

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