[Agda] Small Kernel

[Peter Hancock]

On 05/12/2019 13:48, Jesper Cockx wrote:
> It seems that there is something like ex-falso-quodlibet
>> lurking in the corners of full pattern matching.
> 
> 
> It makes use of the conflict rule from Conor's "constructions on
> constructors" to eliminate impossible cases, is this what you meant?

Something like that, though I don't know Conor's stuff.
I'm just speculating about the mechanics of case splitting
in a state of ignorance and senescence.

vaguely:
I think of the eliminated case clauses as being replaced by
efq terms mapping into the type required where they occur.
I probably think that a comparison between constructor 
tags generates a boolean value c=c'. On a clash, this 
gets mapped by T : bool -> Set to N0, to be the source
of a typeable efq (N0-eliminator) term. On a match, it
gates the correct case clause. 

Perhaps I'm wondering why checking for unhandled cases can't be automated,
and disturbed by coverage/nakedness checking being in bed with termination checking.
However, I've never really understood full-blooded pattern-matching.

-- Peter