--- Day changed Wed Aug 09 2017
carterDolio: byorgey : the changelog entry explaining the exact split flag actually talks about this curly09/08 02:25
carterNicely09/08 02:25
carterDefault 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 induce09/08 02:28
carterI think nonderermistic rewrite systems or backtracking stuff can let you have those ... but agda isn't that afaict09/08 02:28
carter:)09/08 02:28
kclancyNoob 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
kclancyMy 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
kclancyI 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 though09/08 19:08
dolioOh, 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
dolioYeah, I see.09/08 19:22

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