Project

General

Profile

Download (910 Bytes) Statistics
| Branch: | Tag: | Revision:
1
(* ---------------------------------------------------------- *)
2
(* --- Struct 'f_mem_pack'                                --- *)
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
Require Import S_f_reg.
19
Require Import S__arrow_mem_pack.
20

    
21
Record S_f_mem_pack : Type := {
22
                                 F_f_mem_pack__reg : S_f_reg ;
23
                                 F_f_mem_pack_ni_2 : S__arrow_mem_pack
24
}.
25

    
26
Definition IsS_f_mem_pack (S : S_f_mem_pack) : Prop :=
27
    ((IsS__arrow_mem_pack (F_f_mem_pack_ni_2 S))) /\
28
      ((IsS_f_reg (F_f_mem_pack__reg S))).
29

    
(11-11/76)