Ignore:
Timestamp:
Nov 26, 2010, 5:32:34 PM (9 years ago)
Author:
mulligan
Message:

Decidable equality on vectors and its specialisation to bitvectors.

File:
1 edited

Legend:

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

    r314 r315  
    185185nqed.
    186186
     187ndefinition eq_bv ≝
     188  λn: Nat.
     189  λb, c: BitVector n.
     190    eq_v Bool n (λd, e.
     191      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
     192                                                              (negation e)) then
     193        true
     194      else
     195        false) b c.
     196
    187197naxiom plus_minus_inverse_left:
    188198  ∀m, n: Nat.
Note: See TracChangeset for help on using the changeset viewer.