--- Day changed Tue May 02 2017
akr[m]lol I can be so thick at times02/05 12:45
akr[m]I almost asked whether there is something in the standard library which lets us represent a total mapping from one datatype to another02/05 12:46
akr[m]before it dawned on my that we call these things "functions"02/05 12:46
akr[m](or, indeed, maps…)02/05 12:46
akr[m](just an afternoon funny story there ^)02/05 12:49
Saizanakr[m]: too much actual programming?02/05 12:56
Saizanmudri: it tells the termination/productivity checker to stop complaining and the typechecker that it can reduce that definition 02/05 12:58
mudriSaizan: I haven't used {-# TERMINATING #-} much before, but isn't the distinction to {-# NON-TERMINATING #-} the fact that things marked with the former reduce at compile time, whereas things marked with the latter don't?02/05 13:00
akr[m]Saizan: Yeah exactly, in my mind I was looking for a syntactic way to represent this :)02/05 13:00
mudriIf so, I was wondering whether that was troublesome, given that productive functions might not terminate.02/05 13:01
mudriAnd put the type checker in a spin.02/05 13:01
mietekwell… yes02/05 13:02
mietekif you use the pragma to trick Agda into believing something that isn’t true02/05 13:02
mietekthen you’ll just have to perform a termination proof manually, at the meta-level02/05 13:03
mieteki.e. ctrl-C02/05 13:03
mudriSo is there no pragma to assert that a definition is productive?02/05 13:05
Saizanmudri|srcf: "terminating" in agda includes productive02/05 13:22
Saizanmudri|srcf: i.e. if C-c C-n on it will terminate for every input (including variables and whatnot) then you are fine02/05 13:24
Saizanwhat happens for productivity is that definitions by copattern matching, or ones using SHARP, will block computation as you would expect02/05 13:25
mietekSaizan: SHARP meaning musical notation?02/05 14:18
mudriSaizan: late reply, but thanks. That makes sense.02/05 16:13
Saizanmietek: yep02/05 17:38

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