[Agda] Help debugging

[Nils Anders Danielsson]

On 2009-05-06 21:52, Stefan Monnier wrote:
> If I pass the code below to Agda-2.2.2, I get the following error,
> [...]
> Could someone explain to me what's going on and/or how I can get Agda's
> type checker to accept the code?

In cases like this one, where seemingly correct patterns are not
accepted, it can be a good idea to let Agda write the patterns for you
by using case-split. In this case we can see what the problem is just by
replacing the patterns with variables:

  problem : ∀{Δ τ Δ' t} → (P' : Extend (Δ :: τ) Δ') → t ∈ Δ' → ℕ
  problem P' q = ?

If you load this code you will see that Agda cannot infer the type of t.
By giving the type explicitly it is then possible to fill in the
patterns using C-c C-c:

  problem : ∀{Δ τ Δ'} {t : Exp Δ} →
            (P' : Extend (Δ :: τ) Δ') → t ∈ Δ' → ℕ
  problem extBase inHere = {!!}

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.