[Agda] Re: Computation and patterns in called functions

[Francesco Mazzoli]

At Mon, 28 Jan 2013 16:34:53 +0000,
Francesco Mazzoli wrote:
> So in that context you’ll still have ‘.b₁’ and ‘.b₂’, but also a ‘no p’.

On the bus I realised that this doesn’t make sense, in your example you’d have
nothing to reduce after pattern matching so you’ll just expand to the needed
constructors and that’s it - as said you’ll have two booleans in the context
that will look abstracted but are actually two pairs ‘true, false’ and ‘false,
true’, which will make the absurd pattern acceptable.

Apart from that, this implementation might also be too slow, since it’d require
stepping and comparing at each reduction...

Francesco