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

--- Day changed Tue Jul 11 2017
arjen-jonathanIs there an overview of features/fixes scheduled for 2.6.0?11/07 10:50
gallais_akr[m]: I haven't tried nils' (http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html)11/07 12:08
gallais_My goal was not to certify the language recognized but rather start with the Haskell types and see how to make them safe11/07 12:09
akr[m]That one doesn't seem to be updated anymore11/07 12:11
akr[m]Your approach seems more interesting anyway :P11/07 12:12
akr[m]I don't quite understand this, though: https://github.com/gallais/agdarsec/blob/master/src/Text/Parser/Examples/STLC.agda#L7111/07 12:12
akr[m]why do you need to manually prove that something parses?11/07 12:12
akr[m](if I'm understanding the code correctly)11/07 12:12
gallais_These are tests. You don't need to prove anything (in fact these terms where generated by `C-c C-s` or `C-c C-a`, I can't remember)11/07 12:14
gallais_were*11/07 12:14
akr[m]ah I see, thank you11/07 12:15

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