Project

General

Profile

Download (679 Bytes) Statistics
| Branch: | Tag: | Revision:
1
(* ---------------------------------------------------------- *)
2
(* --- Struct 'g_reg'                                     --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
Require Import ZArith.
6
Require Import Reals.
7
Require Import BuiltIn.
8
Require Import bool.Bool.
9
Require Import int.Int.
10
Require Import int.Abs.
11
Require Import int.ComputerDivision.
12
Require Import real.Real.
13
Require Import real.RealInfix.
14
Require Import real.FromInt.
15
Require Import map.Map.
16
Require Import Qedlib.
17
Require Import Qed.
18

    
19
Record S_g_reg : Type := { F_g_reg___g_2 : Z }.
20
Require Import Cint.
21

    
22
Definition IsS_g_reg (S : S_g_reg) : Prop := (is_sint32 (F_g_reg___g_2 S)%Z).
23

    
(17-17/76)