Ignore:
Timestamp:
Dec 5, 2010, 11:54:59 PM (9 years ago)
Author:
sacerdot
Message:

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File:
1 edited

Legend:

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

    r359 r374  
    8282  λn: Nat.
    8383  λ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/.
    8786nqed.
    8887
     
    105104  λb, c: BitVector n.
    106105    full_add n b c false.
    107 
Note: See TracChangeset for help on using the changeset viewer.