--- Day changed Tue May 23 2017
lambda-11235I'm a bit confused, are Agda's datatypes GADTs or inductive families?23/05 00:26
Eduard_Munteanulambda-11235, I'm not entirely sure what you mean, but Agda distinguishes type parameters from type indices.23/05 00:30
mieteklambda-11235: indexed type families23/05 00:31
Eduard_MunteanuFor example, in   data X (i : N) : N -> Set    X has one parameter (i) and one index (unnamed).23/05 00:32
mieteklambda-11235: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.InductiveFamilies23/05 00:33
mieteklambda-11235: why would you think GADTs?23/05 00:33
mieteklambda-11235: note the date on that link23/05 00:33
Eduard_MunteanuIndexes are kinda GADT-ish.23/05 00:33
lambda-11235Eduard_Munteanu, mietek: Thanks.23/05 02:18
mudriIs there a reason why Data.List.Any.Membership uses the propositional equality version of _∈_ , rather than the setoid version?23/05 10:38
mudri(Maybe just that setoids make everything a bit more annoying.)23/05 10:40
TallerGhostWaltexit23/05 17:15
comietekmudri: as far as I can tell, purely for extra pain23/05 20:04
gallais_Could just be bitrot: if the properties were proven before the type was generalised & then the person generalising didn't need the proofs...23/05 20:30

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