Ignore:
Timestamp:
Dec 14, 2011, 2:44:42 PM (8 years ago)
Author:
boender
Message:
  • added alias to ASM/BitVectorTrie
  • removed double include from common/Errors
  • externalised label generation in ASM/Assembly, plus stuff to make it compile
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1600 r1609  
    8989 ]
    9090qed.
    91   
     91 
    9292definition forall
    9393 ≝
    9494  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
    95  
     95
     96alias id "bvt_forall" = "cic:/matita/cerco/ASM/BitVectorTrie/forall.def(4)".
     97
    9698lemma forall_nodel:
    9799  ∀A:Type[0].
Note: See TracChangeset for help on using the changeset viewer.