Move ProofLifiting

parent f0d7addc
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.ProofSamples.ProofLifting (A : Atomic) where
module PiWare.Typed.Semantics.ProofLifting (A : Atomic) where
open import Function using (_∘_; id)
open import Relation.Binary.PropositionalEquality using (_≗_)
......
......@@ -67,7 +67,6 @@ import PiWare.Plugs
--import PiWare.ProofSamples.BoolTrioSeq -- M
import PiWare.ProofSamples.EmptySeq -- M
import PiWare.ProofSamples.EqPlug -- M
import PiWare.ProofSamples.ProofLifting -- M
import PiWare.ProofSamples.RegN.Distribution -- M
import PiWare.ProofSamples.RegN -- M
import PiWare.ProofSamples.RegN' -- M
......@@ -111,6 +110,7 @@ import PiWare.Typed.Samples.BoolTrioComb
import PiWare.Typed.Samples.BoolTrioSeq
import PiWare.Typed.Samples.Muxes
import PiWare.Typed.Semantics.Simulation
import PiWare.Typed.Semantics.ProofLifting -- M
import Relation.Binary.Indexed.Core.Extra
......
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