[Agda] Strict positivity and indices

Dan Doel dan.doel at gmail.com
Wed May 9 18:37:15 CEST 2012


There's a recent thread on coq-club about a certain inductive definition here:


The Agda equivalent is:

    data Val : Set where
      nat : ℕ -> Val
      vec : (l : List Val) -> 0 < length l -> Val

Coq rejects this as not being strictly positive. Agda doesn't complain.

If I understand the proposed explanation, it's that the second
argument has type 0 < length {Val} l, and the arguments to < are
indices, not parameters (and indices are not strictly positive
positions). So my question is: is Coq right, or is Agda?

-- Dan

More information about the Agda mailing list