Changeset 1056 for src/common


Ignore:
Timestamp:
Jul 5, 2011, 4:25:41 PM (9 years ago)
Author:
campbell
Message:

Switch to delayed identifier error scheme.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1055 r1056  
    2222  λtag. mk_universe tag (zero ?) false.
    2323
    24 definition fresh ≝
     24(* Fresh identifier generation uses delayed overflow checking.  To make sure
     25   that the identifiers really were fresh, use the check_universe_ok function
     26   below afterwards. *)
     27definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
    2528  λtag.
    2629  λuniv: universe tag.
     
    3235  //
    3336qed.
     37
     38axiom TooManyIdentifiers : String.
     39
     40definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
     41  λtag, univ.
     42  if counter_overflow ? univ
     43  then Error ? (msg TooManyIdentifiers)
     44  else OK ? it.
    3445
    3546definition eq_identifier ≝
Note: See TracChangeset for help on using the changeset viewer.