Ignore:
Timestamp:
Nov 24, 2010, 3:40:37 PM (9 years ago)
Author:
mulligan
Message:

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File:
1 edited

Legend:

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

    r273 r275  
    210210nqed.
    211211
    212 ncheck bitvector_of_nat.
    213 
    214212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
    215213  match b with
     
    219217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    220218    ].
    221 
    222 (*
    223 nlet rec equality (n: Nat) (b: BitVector n) (c: BitVector n) on b ≝
    224   match b with
    225     [ Empty ⇒
    226       match c return λx.λ_. x = Z → Bool with
    227         [ Empty ⇒ True
    228         | Cons o hd tl ⇒ λabsd1: ?
    229     | Cons
    230     ].
    231 *)
Note: See TracChangeset for help on using the changeset viewer.