--- Day changed Fri Nov 20 2015
tulcodif i force agda to compute a witness of the empty type, e.g. by introducing contradictory notions such as --type-in-type, it doesn't terminate and gets into an infinite loop. what is it doing in that loop? is it searching for something (that it won't find)?20/11 16:47
tulcodor is it constructing some infinitely big element?20/11 16:51
Saizantulcod: depends on how you constructed the witness20/11 16:52
tulcodwell i have a particular example in mind, but i'm rather interested in the general theory behind non-termination here :)20/11 16:52
tulcodi mean. what *can* it be doing?20/11 16:53
Saizani mean, it is reducing that expression to normal form20/11 16:53
Saizanit does not do something clever, it just uses standard evaluation rules20/11 16:54
tulcodSaizan: so are you suggesting that it is reducing further and further subexpressions?20/11 16:54
tulcodof some term whose "normal form" would be infinitely big?20/11 16:55
Saizanit might be big, or it might be small but still a redex20/11 16:56
Saizanthat's why it depends heavily on the term20/11 16:56
Saizani mean, it wouldn't be a normal form in that case20/11 16:57
tulcodSaizan: thanks for your input :)20/11 17:01
tulcodor output, i suppose20/11 17:01
arjen-jonathantulcod what are you upto?20/11 18:05

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