Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1928 r1949  
    8080@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
    8181qed.
    82    
     82
     83include "basics/deqsets.ma".
     84definition Deq_identifier : String → DeqSet ≝ λtag.
     85  mk_DeqSet (identifier tag) (eq_identifier tag) ?.
     86#x#y @eq_identifier_elim /2 by conj/ * #H % [#ABS destruct(ABS) | #G elim (H G)]
     87qed.
     88
     89unification hint 0 ≔ tag; D ≟ Deq_identifier tag
     90(*-----------------------------------------------------*)⊢
     91identifier tag ≡ carr D.
     92
    8393definition word_of_identifier ≝
    8494  λt.
Note: See TracChangeset for help on using the changeset viewer.