# Idris - using an implicit variable inside a function

How can we use an implicit variable inside a function? Reduced to the simplest possible case, is it possible:

```
dim : Vect n a -> Nat
dim vec = n
```

without getting error:

```
When elaborating right hand side of rep:
No such variable n
```

Is there a way to access these values ββfrom the inside? Or is it the same as asking `n`

inside `sin n`

?

In this case, is it possible to prove what `Vect`

is a "bijection" and restores the variables there?

+3

source to share

1 answer

There is no such variable `n`

as it is not limited to pattern matching.

You need to explicitly inject implicit variables into the scope:

```
dim : Vect n a -> Nat
dim {n} vec = n
```

These can be viewed in the idris REPL:

```
*> :set showimplicits
*> :t dim
Main.dim : {n : Prelude.Nat.Nat} -> {a : Type} ->
(__pi_arg : Prelude.Vect.Vect n a) -> Prelude.Nat.Nat
```

+6

source to share