Looking for a value in a tree
Consider the following type:
Require Import ZArith.
Inductive Z_btree : Set :=
| Z_leaf : Z_btree
| Z_bnode : Z->Z_btree->Z_btree->Z_btree.
Define a function taking as argument an integer z
and a tree t:Z_btree and returning true iff t
has (at least) an occurrence of z.
Hint
Use the function Zeq_bool to compare two intergers wrt equality.
formula.
Solution
This file
Note: this solution contains also an infix notation
for these formulae.
Suggestion: add propositional variables !