Ignore:
Timestamp:
Jan 20, 2011, 1:32:32 PM (10 years ago)
Author:
mulligan
Message:

Added bitvector arithmetic for Brian.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r374 r462  
    2626             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
    2727             ]
    28         | Stub s ⇒ λ_. a
    29         ]
     28        | Stub s ⇒ λ_. afg        ]
    3029    ]) (refl ? n).
    3130 ##[##1,2: ndestruct |##*: napply S_inj; //]
Note: See TracChangeset for help on using the changeset viewer.