[Agda] Compile-time parsing

[Nils Anders Danielsson]

On 2011-12-16 12:22, Peter Thiemann wrote:
> That's how I understand Conor's suggestion:
> a metavariable with an empty type like T(false)
> that can never be filled in.

As Conor mentions such a metavariable /can/ sometimes be filled in.
Simple example:

   id-⊥ : ⊥ → ⊥
   id-⊥ x = x

-- 
/NAD