Stream: Coq users

Topic: bool data type

view this post on Zulip zohaze (Jun 03 2023 at 18:02):

Lemma is_x: forall  x l,
f1 x l && f l = true->
In x  l.

Without the information of f1 & f ,could i link bool and proposition?

view this post on Zulip Michael Soegtrop (Jun 05 2023 at 07:37):

No. f1 could be a function which always returns false and f anyway doesn't get x as argument, so it could not possibly tell something about if x is in l.

Last updated: Jun 23 2024 at 05:02 UTC