Stream: Coq users

Topic: empty list


view this post on Zulip zohaze (Oct 12 2021 at 23:59):

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

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 00:20):

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

view this post on Zulip Paolo Giarrusso (Oct 13 2021 at 00:21):

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

view this post on Zulip Ali Caglayan (Oct 13 2021 at 07:48):

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.

view this post on Zulip zohaze (Oct 14 2021 at 04:29):

Thanks for both of you.


Last updated: Jan 29 2023 at 06:02 UTC