Library liblayers.logic.Primitives

Require Import LayerData.
Require Import Structures.
Require Import OptionMonad.
Require Import ErrorMonad.
Require Import liblayers.logic.PseudoJoin.

Section PRIMITIVES.
  Context `{HVE: ReflexiveGraph}.

  Class PrimitiveOps (primsem: V → Type) :=
    {
    }.

  Class Primitives (primsem: V → Type)
      `{primsem_ops: PrimitiveOps primsem}
      `{primsem_sim_op: Sim V E primsem} :=
    {
      prim_quiv_sim_prf :> ReflexiveGraphSim V E primsem
    }.
End PRIMITIVES.