Conversation

eleanor 🌻
@zornsllama
For the record if I make it `last (_::xs@(_::_))` then Idris works it out just fine. I’ll try matching on the implicit parameter tomorrow!
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
eleanor 🌻
@zornsllama
so the top definition works, but if I try to match on the implicit parameter (last') Idris yells at me because `n` is only accessible at compile time :(
last : (n : Nat) -> Vect (S n) a -> a last Z (x::Nil) = x last (S n) (_::xs) = last n xs last' : Vect (S n) a -> a last' {n} xs = last n xs
1
eleanor 🌻
@zornsllama
Idris also doesn't like doing it directly, it says: Error: While processing left hand side of last. Can't match on S ?_ (Erased argument).
last : Vect (S n) a -> a last {n=Z} (x::Nil) = x last {n=S _} (_::xs) = last xs
1
1
Brendan Zabarauskas
@brendanzab
Ohhhh so idris erases implicit variables by default I think. Ie. you can't match on them if they are erased at runtime! I believe there is a way to make these usable at runtime though, lemme check.
2
1
Brendan Zabarauskas
@brendanzab
On I think it is just `{n : Nat} -> Vect (S n) a -> a` - it's the lowercase, auto-generalised variables it automatically sets to be 'erased' (ie. to a 0 multiplicity).
1
2