Changeset 374 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Dec 5, 2010, 11:54:59 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r359 r374 82 82 λn: Nat. 83 83 λb: Bool. 84 ? (pad (S n  (S Z)) (S Z) (Cons Bool ? b (Empty Bool))). 85 nrewrite > plus_minus_inverse_right 86 [ napply (λx.x)  /2/] 84 (pad (S n  (S Z)) (S Z) [[b]])⌈(S n  (S Z)) + S Z ↦ S n⌉. 85 /2/. 87 86 nqed. 88 87 … … 105 104 λb, c: BitVector n. 106 105 full_add n b c false. 107
Note: See TracChangeset
for help on using the changeset viewer.