--- Day changed Sun Dec 17 2017
lengmenHey can I prove the principle of explosion in Agda or do I have to postulate it? I'm currently using this code: `postulate exp : \all {x} -> \bot -> x`17/12 05:51
pgiarrussolensman: there should be one in the stdlib for the false type17/12 11:31
pgiarrussoBut it is basically a pattern match on a value of type empty17/12 11:31
pgiarrussoAnd it should be possible to write that pattern match yourself by case-splitting on a parameter of type False17/12 11:32
pgiarrussoSince False has no constructors, the pattern match needs no cases17/12 11:33
pgiarrussoIf you need to spell this out, you can use the absurd pattern17/12 11:33
pgiarrussoJust write ‘exp ()’ (no quotes) as implementation for your postulate17/12 11:34
pgiarrussoDoh, he left17/12 11:34

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