[Agda] excluded-middle

[Nils Anders Danielsson]

On 2016-06-20 22:57, Martin Escardo wrote:
> [...] but the intuitionistically valid principle that not-not(every
> type has an inhabitant or not).

Or rather "for every type, not not (this type has an inhabitant or
not)".

-- 
/NAD