[Agda] Re: Help debugging

[Ulf Norell]

On Thu, May 7, 2009 at 11:06 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

>
> Could the error in the type signature have been turned into an error?
> Sometimes an unsolved metavariable becomes solved when a hole is filled
> or a new definition is added, so in general I do not think we should
> treat unsolved metavariables as errors (during the development of a
> file). However, in this case I doubt that it is possible to fix the
> problem without changing existing code, and in that case it would be
> more helpful with a proper error message.
>

Adding the following definition will lock down the value of the unsolved
metavariable:

fix : ∀ Δ τ Δ' (t : Exp Δ) → Extend (Δ :: τ) Δ' → t ∈ Δ' → ℕ
fix Δ τ Δ' t = problem {Δ}{τ}{Δ'}{t}

Of course, the original program still won't type check since the
metavariable needs to be solved before checking the inHere pattern. Changing
the pattern to a variable will make everything go through though.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090507/ca48ca17/attachment.html