I have problem in writing this simple statement

a:nat

l:list nat

length [] = (S a)

message: Cannot infer the implicit parameter A of length whose type is "Type" in environment:

l : list nat

a : nat

Actually want to prove( length [] = (S a))-> False

You can prove `forall A, @length A [] = S a -> False.`

Basically, even empty lists must have an element type, and here it wasn't possible to infer one.

`length []`

is ambiguous since there are no elements to infer the type from. Paolo is suggesting you make all implicit arguments for `length`

explicit by writing `@length`

.

Thanks for both of you.

Last updated: Sep 23 2023 at 08:01 UTC