Inductive tree A :=
| leaf: A -> tree A
| forest: list (tree A) -> tree A.
I have this definition of tree
type. And I want to define fixpoint that is True
if tree contains some element x
. (Like In
for lists.)
My first try was failure (with Recursive definition of tree_has_leaf is ill-formed
message):
Fixpoint tree_has_leaf {A} (i: A) (t: tree A) {struct t}: Prop :=
match t with
| leaf _ x => x = i
| forest _ l => Exists (fun x => tree_has_leaf i x) l
end.
Try using fold_right
instead.
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: Oct 05 2023 at 02:01 UTC