Changeset 2177 for src/common


Ignore:
Timestamp:
Jul 12, 2012, 2:56:50 PM (7 years ago)
Author:
campbell
Message:

Tidy up multiplication.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r2176 r2177  
    244244  [ Vint sz1 n1 ⇒ match v2 with
    245245    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    246                     (λn1. Some ? (Vint ? (\snd (vsplit … (multiplication ? n1 n2)))))
     246                    (λn1. Some ? (Vint ? (short_multiplication ? n1 n2)))
    247247                    (None ?)
    248248    | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.