Ignore:
Timestamp:
Aug 10, 2011, 5:17:55 PM (9 years ago)
Author:
campbell
Message:

A little more tidying.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

    r1093 r1104  
    147147  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
    148148
     149(* A predicate that an identifier is in a map, and a failure-avoiding lookup
     150   using it. *)
     151
     152definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     153λtag,A,m,i. lookup … m i ≠ None ?.
     154
     155definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
     156λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     157cases H #H'  cases (H' (refl ??)) qed.
     158
     159
    149160(* Sets *)
    150161
Note: See TracChangeset for help on using the changeset viewer.