Ignore:
Timestamp:
Sep 6, 2011, 5:20:33 PM (8 years ago)
Author:
campbell
Message:

List find function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1092 r1195  
    4646| #h #t #IH #l2 normalize //
    4747] qed.
     48
     49let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
     50match l with
     51[ nil ⇒ None B
     52| cons h t ⇒
     53    match f h with
     54    [ None ⇒ find A B f t
     55    | Some b ⇒ Some B b
     56    ]
     57].
Note: See TracChangeset for help on using the changeset viewer.