A Case Study : binary search trees

The complete development on binary search trees can be found here .
It is also available in Coq's user contributions

Exercises

  1. Exercise 11.1 page 313 Changing inductive definitions
  2. Exercise 11.2 page 314 Certified search trees

Going home
Pierre Castéran