CODEWITHSUNDEEP
idris
bartfrenk
bartfrenk

Reputation: 103

Why doesn't this use of Elem typecheck?

I am quite confused.

module Experiment

import Data.Vect

p1: Elem 5 [3,4,5,6]
p1 = There (There Here)

v : Vect 4 Int
v = 3 :: 4 :: 5 :: 6 :: Nil

p2: Elem 5 v
p2 = There (There Here)

The definition of p2 does not typecheck, while the definition of p1 does. I am using Idris 0.10.2. Is there something I am missing?

Upvotes: 1

Views: 54

Answers (1)

xash
xash

Reputation: 3722

Lowercase names in type declarations are interpreted as implicit arguments (like a in length : List a -> Nat which is actually length : {a : Type} -> List a -> Nat). To refer to the defined Vect you can either use an uppercase name or refer by the namespace:

module Experiment

import Data.Vect

A : Vect 4 Int
A = 3 :: 4 :: 5 :: 6 :: Nil

p2: Elem 5 A
p2 = There (There Here)

a : Vect 4 Int
a = 3 :: 4 :: 5 :: 6 :: Nil

p3: Elem 5 Experiment.a
p3 = There (There Here)

Upvotes: 1

Related Questions