Changeset 464


Ignore:
Timestamp:
Jan 20, 2011, 1:35:13 PM (7 years ago)
Author:
mulligan
Message:

Fixed strange bug/typo in BitVectorTrie?.ma

File:
1 edited

Legend:

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

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