Changeset 2306


Ignore:
Timestamp:
Aug 30, 2012, 4:47:58 PM (7 years ago)
Author:
campbell
Message:

An insertion sort for testing purposes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r2292 r2306  
    334334
    335335
     336(* Not terribly efficient sort for testing purposes *)
     337
     338let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝
     339match l with
     340[ nil ⇒ [a]
     341| cons h t ⇒ if lt a h then a::h::t else h::(ordered_insert A lt a t)
     342].
     343
     344let rec insert_sort (A:Type[0]) (lt:A → A → bool) (l:list A) on l : list A ≝
     345match l with
     346[ nil ⇒ [ ]
     347| cons h t ⇒ ordered_insert A lt h (insert_sort A lt t)
     348].
Note: See TracChangeset for help on using the changeset viewer.