From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Environment.
From Velus Require Import Clocks.
From Velus Require Export IndexedStreams.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import CoreExpr.CETyping.
From Velus Require Import CoreExpr.CESemantics.
From Velus Require Import CoreExpr.CEIsFree.

Import List.

Properties of Core Expressions

Module Type CEPROPERTIES
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Syn : CESYNTAX Ids Op OpAux Cks)
       (Import Str : INDEXEDSTREAMS Ids Op OpAux Cks)
       (Import Sem : CESEMANTICS Ids Op OpAux Cks Syn Str)
       (Import Typ : CETYPING Ids Op OpAux Cks Syn)
       (Import IsF : CEISFREE Ids Op OpAux Cks Syn).


















End CEPROPERTIES.

Module CEProperties
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Syn : CESYNTAX Ids Op OpAux Cks)
       (Str : INDEXEDSTREAMS Ids Op OpAux Cks)
       (Sem : CESEMANTICS Ids Op OpAux Cks Syn Str)
       (Typ : CETYPING Ids Op OpAux Cks Syn)
       (IsF : CEISFREE Ids Op OpAux Cks Syn)
       <: CEPROPERTIES Ids Op OpAux Cks Syn Str Sem Typ IsF.
  Include CEPROPERTIES Ids Op OpAux Cks Syn Str Sem Typ IsF.
End CEProperties.