Ignore:
Timestamp:
Mar 7, 2013, 1:07:31 PM (7 years ago)
Author:
campbell
Message:

Tidy up Measurable.ma a little, get rid of obsolete comments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r2443 r2800  
    244244]
    245245qed.
     246
     247
     248
     249lemma flatten_append : ∀A,l1,l2.
     250  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
     251#A #l1 #l2
     252elim l1
     253[ %
     254| #h #t #IH whd in ⊢ (??%(??%?));
     255  change with (flatten ??) in match (foldr ?????); >IH
     256  change with (flatten ??) in match (foldr ?????);
     257  >associative_append %
     258] qed.
    246259
    247260
     
    352365
    353366
    354 (* Not terribly efficient sort for testing purposes *)
     367(* A not terribly efficient sort for testing purposes *)
    355368
    356369let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝
Note: See TracChangeset for help on using the changeset viewer.