Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / S__arrow_mem_pack.v @ 6a93d814

History | View | Annotate | Download (753 Bytes)

1
(* ---------------------------------------------------------- *)
2
(* --- Struct '_arrow_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__arrow_reg.
19

    
20
Record S__arrow_mem_pack : Type := { F__arrow_mem_pack__reg : S__arrow_reg }.
21

    
22
Definition IsS__arrow_mem_pack (S : S__arrow_mem_pack) : Prop :=
23
    (IsS__arrow_reg (F__arrow_mem_pack__reg S)).
24