/home/laney/.irssi/irclogs/Freenode/#agda.log-20170723

--- Day changed Sat Jul 22 2017
petercommandhttps://github.com/UlfNorell/x86-agda/blob/master/src/X86/Common.agda#L8322/07 04:29
petercommandwhere is the (| ... |) defined?22/07 04:30
petercommandI think it must not be function definition? because you can't have parentheis in funciton application22/07 04:31
petercommand*function application22/07 04:31
adamsepetercommand: I think it's a language feature that was added in a recent Agda (idiom brackets)22/07 10:40
petercommandadamse: thx!22/07 10:58
rntzhm, now I want to know how idiom brackets work22/07 11:20
rntzthey don't appear to be described in agda.readthedocs.io22/07 11:22
adamserntz: https://github.com/agda/agda/blob/master/CHANGELOG.md#language-1 a bit further down22/07 11:33
rntzoh, wow, the feature I wanted earlier *is* present, it's called "result splitting" and you can do it with C-c C-c RET22/07 11:39
rntzI should read the agda changelogs, I guess22/07 11:40
rntzadamse: thanks!22/07 11:40
comietekrntz: I thought you tried that22/07 13:35
comietekrntz: i never remember which key combo is it; sorry22/07 13:35
petercommandis there any way to control expression unfolding besides using abstract?22/07 13:37
petercommandI want my expression to unfold one time22/07 13:39
petercommandI don't want too much unfolding, but I want some expression unfolding22/07 13:39
comietekpetercommand: not sure if I understand, but maybe define your expression-to-unfold based on a postulate? evaluation will stop at the postulate22/07 13:51
comietekpetercommand: similarly, a module parameter22/07 13:51
petercommandright, and I will need to add manual rewrite rules to manually unfold my expression22/07 13:56
comietekright, I think I saw someone do something like this22/07 13:57
petercommandsaw a similar issue on agda mailing list https://lists.chalmers.se/pipermail/agda/2012/003976.html22/07 13:58
petercommandcomietek: any links to that?22/07 14:04
petercommandwould like to see how other people are doing this22/07 14:04
comietekhard to search for22/07 14:05
petercommandalright22/07 14:06
petercommandmanually adding rewrite rules is really cumbersome, I have to add one more rule for every pattern in a function22/07 14:42
comietekit's probably not the usual way to do things22/07 14:55
petercommandwhat's the usual way to do things then?22/07 15:00
comietekpetercommand: through evaluation.22/07 15:16
mckeankylejIf you encode the natural numbers as: Nat = {A : Set} -> (A -> A) -> A -> A22/07 15:17
mckeankylejhow do you write the principal of induction?22/07 15:18
mckeankylejWith data encoded naturals it looks something like induction : (P : Nat -> Set) -> P Z -> ({k : Nat} -> P k -> P (S k)) -> (n : Nat) -> P n22/07 15:19
petercommandcomietek: but then if the term gets normalized, the term gets too big, and I want to operate on a higher level, not the fully normalized term22/07 15:19
petercommand*not on22/07 15:19
comietekpetercommand: what are you doing?22/07 15:20
petercommandcomietek: monadic programming22/07 15:21
doliomckeankylej: You don't.22/07 15:21
comietekpetercommand: it sounds like you would like to work with a method to explicitly pause/resume evaluation22/07 15:21
petercommandyes22/07 15:21
comietekpetercommand: or, in other words, with quotation22/07 15:21
petercommandquotation?22/07 15:21
mckeankylejdolio: is it possible to prove things about the church encoded naturals?22/07 15:21
petercommandthe reflection stuff?22/07 15:22
comietekpetercommand: have you looked at Agda's reflection?22/07 15:22
petercommandno22/07 15:22
dolioWell, some things, certainly. :)22/07 15:22
comietekpetercommand: unfortunately that is the best we have in Agda22/07 15:22
mckeankylejlike can I do this: plusRightZero : (n : Nat) -> n = n + z with church encoded naturals?22/07 15:22
comietekpetercommand: I am doing research into quotation22/07 15:22
comietekpetercommand: Lean could also interest you22/07 15:22
dolioBut you can't write the induction principle in Agda. At least not right now.22/07 15:22
comietekpetercommand: it has well-developed facilities for writing tactics / metaprograms22/07 15:23
mckeankylejdolio: why is that?22/07 15:23
dolioSaizan has code that implements internalized parametricity, and that would allow you to write the induction principle. But I don't think it's been merged (maybe I'm wrong).22/07 15:23
petercommandheard people mention Lean a couple of times, but never tried it..perhaps it's time for me to try it :322/07 15:23
dolioThe other problem is that that is arguably not even the natural numbers.22/07 15:25
dolioBecause of Agda's predicativity.22/07 15:25
mckeankylejI was worried about that22/07 15:25
doliomckeankylej: Anyhow, I think I once saw a paper that induction on the naturals cannot be written in the calculus of constructions.22/07 15:28
dolioI've had trouble finding the paper subsequently when looking for it, though.22/07 15:29
dolioOh well.22/07 15:38
doliohttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.435522/07 15:38
dolioIf they come back.22/07 15:38
comietekdolio: appreciate the link22/07 16:06
Nik05[m]Hey [comietek](https://matrix.to/#/@freenode_comietek:matrix.org) , a little busy now with work. But still watching some lectures about formal logics. Next week I will try it out on Agda22/07 16:32

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