Changeset 11 for Csemantics/extralib.ma
 Timestamp:
 Jul 7, 2010, 12:55:01 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/extralib.ma
r10 r11 267 267 ##] nqed. 268 268 269 naxiom Z_times : Z → Z → Z. 269 ndefinition Z_times : Z → Z → Z ≝ 270 λx,y. match x with 271 [ OZ ⇒ OZ 272  pos n ⇒ 273 match y with 274 [ OZ ⇒ OZ 275  pos m ⇒ pos (n*m) 276  neg m ⇒ neg (n*m) 277 ] 278  neg n ⇒ 279 match y with 280 [ OZ ⇒ OZ 281  pos m ⇒ neg (n*m) 282  neg m ⇒ pos (n*m) 283 ] 284 ]. 270 285 interpretation "integer multiplication" 'times x y = (Z_times x y). 271 286
Note: See TracChangeset
for help on using the changeset viewer.