Stream: Coq users

Topic: ✔ tree membership prop

Lessness (Jul 17 2022 at 21:03):

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.

Notification Bot (Jul 17 2022 at 21:06):

Lessness has marked this topic as resolved.

Gaëtan Gilbert (Jul 17 2022 at 21:10):

(probably you want or/False not and/True)

Lessness (Jul 17 2022 at 21:33):

Gaëtan Gilbert said:

(probably you want or/False not and/True)

Yes, thank you!

Last updated: Jan 29 2023 at 01:02 UTC