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

--- Day changed Tue May 16 2017
lpasteaaa pasted “fil” at http://lpaste.net/822963822514929664016/05 10:12
lpasteaaa pasted “ss” at http://lpaste.net/771270991575148134416/05 10:54
{AS}@mods16/05 11:03
lambdabotMaybe you meant: todo more docs16/05 11:03
{AS}@ops *16/05 11:03
lambdabotMaybe you meant: pl oeis docs16/05 11:03
lpasteaaa pasted “asd” at http://lpaste.net/14968137549715865616/05 14:39
{AS}Saizan: ^16/05 14:42
{AS}Can we block these? (I saw you were an OP :) )16/05 14:42
byorgey{AS}: note on lpaste.net there's a link for reporting a post as spam16/05 14:49
{AS}byorgey: Thanks!16/05 14:50
byorgeyIt's not specific to Agda at all and I don't think the maintainer hangs out in here16/05 14:50
gallais_they're doing what they can: https://www.reddit.com/r/haskell/comments/5r9fhy/lpastes_spam_filtering/16/05 14:53
gallais_If you report the spam, it should learn to block it :)16/05 14:53
{AS}Ah, great16/05 14:56
lpasteaaa pasted “sa” at http://lpaste.net/892672309101120716816/05 15:09
gallais_16:07 < lpaste> aaa pasted “sa” at http://lpaste.net/892672309101120716816/05 18:43
gallais_This one for instance has been nuked. It would be nice though if the analysis were run *before* posting to the irc channel16/05 18:43
byorgeygallais_: I think it is.  Someone must have reported that as spam after it was posted.16/05 19:40
pgiarrussogallais_: does your repo prove that (parallel) substitution commutes with evaluation? I'm taking a quick look at the paper and https://github.com/gallais/type-scope-semantics/blob/master/src/Properties/Fusable/Instances.agda, but I'm not sure why there's no lemma using fusableSubstitutionNormalise16/05 20:49
pgiarrussoI guess one could write analogues of fuseRenamingEvaluate and fuseRenamingNormalise, which have more readable statements, but it's not obviously a one-minute affair _for me at this moment_16/05 20:54

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