idris-lang / Idris2

A purely functional programming language with first class types

https://idris-lang.org/

Other

2.53k stars 380 forks source link

Closed m-rinaldi closed 5 months ago

m-rinaldi commented 5 months ago

Description

The following length:

length : Vect n elem -> Nat
length {n} xs = n

produces the following error on Idris 2:

Error: While processing right hand side of length. n is not accessible in this context.

Turning n into a bound implicit name behaves as described in the book.