Thank you! It worked like a charm.
Fixpoint tree_has_leaf {A} (i: A) (t: tree A) {struct t}: Prop :=
match t with
| leaf _ x => x = i
| forest _ l => fold_right (fun x => and (tree_has_leaf i x)) True l
end.
Lessness has marked this topic as resolved.
(probably you want or
/False
not and
/True
)
Gaëtan Gilbert said:
(probably you want
or
/False
notand
/True
)
Yes, thank you!
Last updated: Jan 29 2023 at 01:02 UTC