Ignore:
Timestamp:
Nov 29, 2010, 2:08:52 PM (9 years ago)
Author:
mulligan
Message:

Fixed segmentation fault in Nat.ma, added get_index and renamed previous get_index to get_index_weak in List.ma.

File:
1 edited

Legend:

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

    r320 r330  
    195195        false) b c.
    196196
    197 naxiom plus_minus_inverse_left:
    198   ∀m, n: Nat.
    199     (m + n) - n = m.
    200    
    201 naxiom plus_minus_inverse_right:
    202   ∀m, n: Nat.
    203     (m - n) + n = m.
    204 
    205 naxiom greater_than_b: Nat → Nat → Bool.
    206 
    207197nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
    208198  let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
Note: See TracChangeset for help on using the changeset viewer.