zohaze (Oct 12 2021 at 23:59): 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
Paolo Giarrusso (Oct 13 2021 at 00:20):You can prove forall A, @length A [] = S a -> False.
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.
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.
zohaze (Oct 14 2021 at 04:29):Thanks for both of you.
Last updated: Oct 13 2024 at 01:02 UTC