pianke (Jul 08 2022 at 07:51): pianke (Jul 08 2022 at 07:51):I am applying command
pose proof list_max_le l (list_max l) as H. Then H become
H : List.list_max l <= list_max l -> Forall (fun k : nat => k <= list_max l) l instead of
list_max l <= list_max l <-> Forall (fun k : nat => k <= list_max l) l .
How i can remove List . from above H?
Pierre Castéran (Jul 08 2022 at 09:42):Did you try Locate list_max ? You may have more than one function with base name list_max.
pianke (Jul 08 2022 at 11:40):Against :Locate list_max .
I get this message "Constant filename_v.list_max Constant Coq.Lists.List.list_max shorter name to refer to it in current context is List.list_max))
I am using these two definitions only
Definition list_max l := fold_right max 0 l.
Lemma list_maxs b l : In b l -> b <= list_max l.
Pierre Castéran (Jul 08 2022 at 12:05):It certainly comes from your re-definition of list_max (useless, since it's the same fold_rightas in List).
Just try to remove it.
pianke (Jul 13 2022 at 18:17):Ok,thanks
Last updated: Jan 29 2023 at 01:02 UTC