Changeset 15 for C-semantics/binary


Ignore:
Timestamp:
Jul 22, 2010, 4:50:06 PM (10 years ago)
Author:
campbell
Message:

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/binary/Z.ma

    r10 r15  
    151151nqed.
    152152
    153 ndefinition Zle : Z → Z → Prop ≝
    154 λx,y:Z.
     153nlet rec Zle (x:Z) (y:Z) on x : Prop ≝
    155154  match x with
    156155  [ OZ ⇒
     
    173172interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
    174173
    175 ndefinition Zlt : Z → Z → Prop ≝
    176 λx,y:Z.
     174nlet rec Zlt (x:Z) (y:Z) on x : Prop ≝
    177175  match x with
    178176  [ OZ ⇒
     
    306304
    307305(* boolean equality *)
    308 ndefinition eqZb : Z → Z → bool ≝
    309 λx,y:Z.
     306nlet rec eqZb (x:Z) (y:Z) on x : bool ≝
    310307  match x with
    311308  [ OZ ⇒
     
    364361nqed.
    365362
    366 ndefinition Z_compare : Z → Z → compare ≝
    367 λx,y:Z.
     363nlet rec Z_compare (x:Z) (y:Z) : compare ≝
    368364  match x with
    369365  [ OZ ⇒
     
    422418nqed.
    423419
    424 ndefinition Zplus : Z → Z → Z ≝
    425   λx,y. match x with
     420nlet rec Zplus (x:Z) (y:Z) on x : Z ≝
     421  match x with
    426422    [ OZ ⇒ y
    427423    | pos m ⇒
Note: See TracChangeset for help on using the changeset viewer.