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.


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