Changeset 15 for Csemantics/binary
 Timestamp:
 Jul 22, 2010, 4:50:06 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/binary/Z.ma
r10 r15 151 151 nqed. 152 152 153 ndefinition Zle : Z → Z → Prop ≝ 154 λx,y:Z. 153 nlet rec Zle (x:Z) (y:Z) on x : Prop ≝ 155 154 match x with 156 155 [ OZ ⇒ … … 173 172 interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)). 174 173 175 ndefinition Zlt : Z → Z → Prop ≝ 176 λx,y:Z. 174 nlet rec Zlt (x:Z) (y:Z) on x : Prop ≝ 177 175 match x with 178 176 [ OZ ⇒ … … 306 304 307 305 (* boolean equality *) 308 ndefinition eqZb : Z → Z → bool ≝ 309 λx,y:Z. 306 nlet rec eqZb (x:Z) (y:Z) on x : bool ≝ 310 307 match x with 311 308 [ OZ ⇒ … … 364 361 nqed. 365 362 366 ndefinition Z_compare : Z → Z → compare ≝ 367 λx,y:Z. 363 nlet rec Z_compare (x:Z) (y:Z) : compare ≝ 368 364 match x with 369 365 [ OZ ⇒ … … 422 418 nqed. 423 419 424 n definition Zplus : Z → Z →Z ≝425 λx,y.match x with420 nlet rec Zplus (x:Z) (y:Z) on x : Z ≝ 421 match x with 426 422 [ OZ ⇒ y 427 423  pos m ⇒
Note: See TracChangeset
for help on using the changeset viewer.