--- Day changed Mon Aug 07 2017
rntzagda can't internalize the fact that, say, equality on functions is undecidable, can it?07/08 16:41
rntzit can't prove \neg (Dec (_\equiv_ {a -> b}))07/08 16:42
rntzwtb: deriving decidable07/08 17:41
jonsterlingrntz: Because Agda has models which would refute that principle, I think it is not derivable. Unless I misread :) 07/08 23:32

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