Certified search trees
Consider the development in searchtrees.v .
Define a type for search trees in sort Set>, and
consider new specifications for occur test, insertion and deletion.
Solution
The development search_set.v
contains the definition of a type sch_tree in sort
Set, and defines new specifications named
sch_insert_spec, sch_rm_spec, etc.
It ends with two functions transforming the older specifications into the
new ones, and viceversa.
Going home
Pierre Castéran