Ignore:
Timestamp:
Nov 23, 2010, 6:12:10 PM (9 years ago)
Author:
mulligan
Message:

More added.

File:
1 edited

Legend:

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

    r269 r270  
    200200        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    201201    ].
     202   
     203nlet rec equality (n: Nat) (b: BitVector n) (c: BitVector n) on b ≝
     204  match b with
     205    [ Empty ⇒
     206      match c return λx.λ_. x = Z → Bool with
     207        [ Empty ⇒ True
     208        | Cons o hd tl ⇒ λabsd1: ?
     209    | Cons
     210    ].
Note: See TracChangeset for help on using the changeset viewer.