Ignore:
Timestamp:
Feb 16, 2011, 4:25:00 PM (8 years ago)
Author:
campbell
Message:

Make stuff from D4.1 work with my copy of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/Arithmetic.ma

    r475 r533  
    2828    let cy_flag ≝ geb result_old (2^n) in
    2929    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    30       mk_pair ? ? (bitvector_of_nat n result)
     30      pair ? ? (bitvector_of_nat n result)
    3131                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3232
     
    111111        Some ? (bitvector_of_nat n result)
    112112    ].
    113    
    114 alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)".
    115      
    116 definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝
     113     
     114definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
    117115  λn.
    118116    match n with
Note: See TracChangeset for help on using the changeset viewer.