Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r753 r757  
    2424      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    2525// qed.
     26
     27definition eq_identifier ≝
     28  λt.
     29  λl, r: identifier t.
     30  match l with
     31  [ an_identifier l' ⇒
     32    match r with
     33    [ an_identifier r' ⇒
     34      eq_bv ? l' r'
     35    ]
     36  ].
     37   
     38   
     39definition word_of_identifier ≝
     40  λt.
     41  λl: identifier t.
     42  match l with   
     43  [ an_identifier l' ⇒ l'
     44  ].
    2645
    2746definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
Note: See TracChangeset for help on using the changeset viewer.