--- Day changed Fri Jul 21 2017
arjen-jo1Is the fact that Agda doesn't support coercive subtyping a design choice or just not yet considered/implemented?21/07 11:03
rntzarjen-jonathan: what do you mean by coercive subtyping?21/07 12:38
BoardersI am just messing around with agda for the first time trying to define the not function21/07 13:37
Boardershow do I get it to pattern match from a hole?21/07 13:38
Boardersoh I think I figured it out (C-c C-c after inputting the argument variable)21/07 13:39
rntzhm. is there an equivalent of C-c C-c for copattern definitions in agda-mode?21/07 16:36
rntz"I am defining a record, please split this definition into 'cases' for each field"21/07 16:36
rntzso if I currently have: (foo : A x B; foo = ?) and I put my cursor in the hole and "copattern-case" I get (foo : A x B; proj1 foo = ?; proj2 foo = ?)21/07 16:37
rntzit's like refine, but with copatterns, I guess.21/07 16:38
dolioI don't recall seeing it last time I was looking at the commands.21/07 16:38
dolioUnless one of the other commands does it.21/07 16:38
petercommandhttps://github.com/UlfNorell/x86-agda/blob/master/src/X86/Typed.agda#L5421/07 16:43
petercommandwhat is this syntax?21/07 16:43
petercommand[rax]  initS = %rax21/07 16:44
petercommandit's so weird...it can't be an argument to initS21/07 16:46
dolioThat's definition of initS by copatterns.21/07 16:50
dolio[rax] is a field of the record type being defined.21/07 16:51
petercommandthx, I will look into copatterns :321/07 16:53
comietekrntz: refine? C-c C-r21/07 16:59
rntzcomietek: 21/07 18:06
rntzargh, connection issues21/07 18:06
rntzcomietek: refine will introduce a record rather than splitting the defined name into copatterns21/07 18:06
rntzso if I have (foo : A x B; foo = ?) and refine, I get (foo : A x B; foo = ? , ?) rather than (foo : A x B; proj1 foo = ?; proj2 foo = ?)21/07 18:07
rntzfor pairs, this is usually fine :)21/07 18:07
rntzbut for more complex records, copatterns can be more readable IMO21/07 18:07
comietekhave you defined the record as codata?21/07 18:08
rntzhm? no, it's not codata.21/07 18:08
rntzI mean, it's a record type. but it's not marked specially or anything. how do you mark a record as codata?21/07 18:09
rntz"coinductive" or something?21/07 18:09
rntzhm, even after marking it coinductive C-c C-r doesn't do copattern-splitting, it just introduces a (record { ... }) form21/07 18:11
dolioYour record doesn't need to be coinductive to use copatterns.21/07 18:23
dolioSo that'd be an annoying limitation.21/07 18:23
dolioSee the code petercommand pasted, for instance, which uses copatterns to define an inductive record.21/07 18:23
rntzyeah, I have not really touched coinduction in agda, but I have used copatterns a lot21/07 21:08
rntzwell, "a lot" since learning about them last week21/07 21:08
rntzhm, maybe longer than that. anyway.21/07 21:09
rntzokay, that's weird21/07 22:09
rntzI have a hole that, when I stick a term `foo` into it and hit C-c C-r to refine, it says it can't refine21/07 22:10
rntzbut if I just remove the hole and manually write `foo` there, it typechecks21/07 22:10
rntzis this a bug?21/07 22:10
comietekthere are a number of situations like that21/07 23:00
comietekI've been reporting them as bugs21/07 23:01
comieteksome of them were fixed; maybe even all21/07 23:01
comietekbut I know there are some left that I wasn't able to report in a useful way21/07 23:01
rntzwell, I bug-reported it https://github.com/agda/agda/issues/265321/07 23:09
rntzit's pretty well minified, I think21/07 23:09

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