diff options
Diffstat (limited to 'Data/Circuit.agda')
| -rw-r--r-- | Data/Circuit.agda | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/Data/Circuit.agda b/Data/Circuit.agda index 0be86f9..09dfb2e 100644 --- a/Data/Circuit.agda +++ b/Data/Circuit.agda @@ -12,15 +12,16 @@ open import Data.Fin using (Fin) open import Data.Hypergraph {c} {ℓ} Gates using ( Hypergraph - ; mkHypergraph ; Hypergraphₛ + ; mkHypergraphₛ + ; List∘Edgeₛ ; module Edge - ; normalize + ; mkHypergraph ; _≈_ ; mk≈ ) open import Data.Nat using (ℕ) -open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary using (Setoid) open import Function.Bundles using (Func; _⟶ₛ_) open List using (List) @@ -35,6 +36,9 @@ map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges) Circuitₛ : ℕ → Setoid c (c ⊔ ℓ) Circuitₛ = Hypergraphₛ +mkCircuitₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Circuitₛ n +mkCircuitₛ = mkHypergraphₛ + open Func open Edge.Sort using (sort) |