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

--- Day changed Sun Jul 16 2017
jonsterlingrntz: It's semantically equivalent to the usual notation; the reason it's preferred is that really deep definitions become more readable.16/07 00:28
jonsterlingcarter: Copatterns actually shine really nicely already for flat / non-coinductive records. Doing algebra and category theory is much nicer this way, because you don't need auxiliary definitions as much—whereas any time you want to do some serious pattern matching, especially involving 'with', ordinary lambda abstraction will fall down.16/07 00:29
jonsterlingrntz, mietek: I only learned about it by reading freebroccolo's code, and I assume he learned about it by watching the development of Agda HEAD.16/07 00:30
mckeankylejI am having some trouble making valid with statements can someone help me? The code and error is in this lpaste: http://lpaste.net/35696116/07 04:04
comietekjonsterling: do you have an example of serious pattern matching with with?16/07 10:14
rntzjonsterling: hm, ok. the postfix style to me doesn't seem much more readable than the prefix style16/07 20:00
rntzbut I guess style is always subjective :P16/07 20:00
mietekrntz: yeah16/07 20:21
mietekrntz: I’m not sure about it either16/07 20:21
mietekit is unfortunate how much it looks like node.js16/07 20:22
eriscohow powerful is the automatic proof search? I understand Agda has some reflection system that does this16/07 22:19
jonsterlingmietek, rntz I think the postfix style really only helps when you're working with some fairly deep structures, and if you are interleaving pattern matching with copattern matching; before that, it doesn't seem to add much. 16/07 22:41
mietekjonsterling: yes. show me the code!16/07 22:41
jonsterlingmietek: this repo probably has some examples in it: https://github.com/freebroccolo/agda-cubical-sets16/07 22:42
mietekerisco: Agsy is a fully-automated proof search procedure that is able to fill in some holes in Agda code.16/07 22:43
mietekerisco: Wouter Swierstra’s paper on "Auto in Agda" uses the previous-generation reflection facilities of Agda to implement some sort of proof search procedure, as well16/07 22:43
mietekerisco: in general, automation for Agda is not nearly as well developed as for Coq, Isabelle, or Lean16/07 22:43
mietekerisco: there doesn’t seem to be any reason why automation couldn’t be developed for Agda; it seems to be a matter of time and energy16/07 22:44
eriscojonsterling, so this is where you hang out!16/07 22:46
mieteklook for the video of Leo’s talk on metaprogramming in Lean last week; https://www.newton.ac.uk/seminar/2017071210001100116/07 22:46
mietekhe showed examples of how to write automation for Lean in Lean’s metalanguage16/07 22:46
mietekand these should be portable to Agda, with sufficient pain16/07 22:46
mieteker, motivation16/07 22:46
mietekit doesn’t seem like any of the ATP people are looking in this direction, though16/07 22:47
mietekand I asked16/07 22:48
mietekthe idea of generating proof terms for the user to look at, as Agsy does, seems barely thinkable16/07 22:48
mietekeven though Sledgehammer does a similar sort of thing when generating "structured proofs" for Isabelle16/07 22:49
eriscomietek, okay, thanks16/07 22:49
mietekbut these "structured proofs" are still stringed-together invocations of tactics16/07 22:49
mietekso, imperative scripts, and not declarative proofs16/07 22:56
mietekeven though they call them "declarative"16/07 22:56

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