Move Simulation/Equality to Simulation/Equivalence

parent 963ab2ff
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Equality (A : Atomic) where
module PiWare.Semantics.Simulation.Equivalence (A : Atomic) where
open import Function using (_∘_; _∘′_; _⟨_⟩_)
open import Data.Product using (_×_; uncurry′)
......
......@@ -21,7 +21,7 @@ open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Plugs using (id⤨; nil⤨₀)
open import PiWare.Patterns.Id using (adaptEqI; adaptEqO; adaptEqIO)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧[_])
open import PiWare.Semantics.Simulation.Equality A using (_≅[_]_; _≊[_]_; _≋[_]_; refl≋; ≅⇒≋; ≋-refl; ≋-sym)
open import PiWare.Semantics.Simulation.Equivalence A using (_≅[_]_; _≊[_]_; _≋[_]_; refl≋; ≅⇒≋; ≋-refl; ≋-sym)
open import PiWare.Semantics.Simulation.Properties.Plugs A using (id⤨⫃id[_]; id⤨⫅id[_])
\end{code}
......
......@@ -33,7 +33,7 @@ open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Plugs using (plug-Vecη; id⤨)
open import PiWare.Semantics.Simulation A using (W; W⟶W; ⟦_⟧[_]; ⟦_⟧ᶜ[_]; ⟦_⟧ω[_]) renaming (module WithGates to SimulationWithGates)
open import PiWare.Semantics.Simulation.Compliance A using (_⫅[_]_; _⫃[_]_) renaming (module WithGates to ComplianceWithGates)
open import PiWare.Semantics.Simulation.Equality A using (_≅[_]_; _≋[_]_; ≅⇒≋; ≋-refl; ≋-trans) renaming (module WithGates to EqWithGates)
open import PiWare.Semantics.Simulation.Equivalence A using (_≅[_]_; _≋[_]_; ≅⇒≋; ≋-refl; ≋-trans) renaming (module WithGates to EqWithGates)
\end{code}
......
......@@ -10,7 +10,7 @@ open import PiWare.Plugs using (id⤨₁)
open import PiWare.Circuit using (C[_]; _⟫_; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.Simulation.Equality A using (_≋[_]_)
open import PiWare.Semantics.Simulation.Equivalence A using (_≋[_]_)
\end{code}
......
......@@ -18,7 +18,7 @@ open import PiWare.Plugs using (id⤨₁)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.Simulation.Semigroup.Base A using (C₂[_]; IsSemigroupC₂[_]; SemigroupC₂)
open import PiWare.Semantics.Simulation.Equality A using (_≅[_]_; ≅⇒≋)
open import PiWare.Semantics.Simulation.Equivalence A using (_≅[_]_; ≅⇒≋)
\end{code}
......
......@@ -77,7 +77,7 @@ import PiWare.Semantics.AreaAnalysis.Nand
import PiWare.Semantics.AreaAnalysis
import PiWare.Semantics.Simulation.BoolTrio
import PiWare.Semantics.Simulation.Compliance
import PiWare.Semantics.Simulation.Equality
import PiWare.Semantics.Simulation.Equivalence
import PiWare.Semantics.Simulation.Nand
import PiWare.Semantics.Simulation.Properties.Extension
import PiWare.Semantics.Simulation.Properties.Plugs
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment