I have problem in writing this simple statement
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
Thanks for both of you.
Last updated: Jan 29 2023 at 06:02 UTC