Changeset 2306 for src/utilities
 Timestamp:
 Aug 30, 2012, 4:47:58 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r2292 r2306 334 334 335 335 336 (* Not terribly efficient sort for testing purposes *) 337 338 let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝ 339 match 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 344 let rec insert_sort (A:Type[0]) (lt:A → A → bool) (l:list A) on l : list A ≝ 345 match 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.