Changeset 533 for Deliverables/D3.1/Csemantics/cerco/Arithmetic.ma
 Timestamp:
 Feb 16, 2011, 4:25:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/cerco/Arithmetic.ma
r475 r533 28 28 let cy_flag ≝ geb result_old (2^n) in 29 29 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) 31 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 32 32 … … 111 111 Some ? (bitvector_of_nat n result) 112 112 ]. 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 114 definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ 117 115 λn. 118 116 match n with
Note: See TracChangeset
for help on using the changeset viewer.