Changeset 9 for Csemantics/Integers.ma
 Timestamp:
 Jun 21, 2010, 4:22:09 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Integers.ma
r4 r9 94 94 [modulus] (excluded. *) 95 95 96 nrecord int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus}.96 nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }. 97 97 98 98 (* The [unsigned] and [signed] functions return the Coq integer corresponding … … 110 110 machine integer. The argument is treated modulo [modulus]. *) 111 111 (* TODO: prove *) 112 naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus. 112 (*naxiom repr : Z → int.*) 113 114 (*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*) 113 115 114 116 ndefinition repr : Z → int := λx. 115 mk_int (x \mod modulus) ?(*Z_mod_lt x modulus modulus_pos*).116 napply repr_ax.117 nqed. 117 mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*). 118 (*napply repr_ax. 119 nqed.*) 118 120 119 121 ndefinition zero := repr 0.
Note: See TracChangeset
for help on using the changeset viewer.