Skip to content

Add simplification instance for list ≠ [], needed for quicksort

Ike Mulder requested to merge ci/simpl_quicksort into master

When doing the quicksort exercise, RefinedC would at some point get stuck on a goal of the form some_list ≠ [] ∧ …, where some_list is a protected evar. This merge request adds an instance simplifying l ≠ [] into ∃ a l', l = a :: l' whenever l is a protected evar.

Additionally, it adds the sorting function to tutorial/quicksort_solution.c for which this instance was necessary.

Merge request reports