aboutsummaryrefslogtreecommitdiff
path: root/Data/Hypergraph/Base.agda
diff options
context:
space:
mode:
authorJacques Comeaux <jacquesrcomeaux@protonmail.com>2025-10-28 17:20:33 -0500
committerJacques Comeaux <jacquesrcomeaux@protonmail.com>2025-10-28 17:20:33 -0500
commit0bf55c23ad3bee621d0e7425f5a5e875254e3450 (patch)
treeea5dbac95aa1fa9449b785cb5be3078790a88aea /Data/Hypergraph/Base.agda
parent2cd74f160389fe2ab2b30ab628fbb9b712f06faf (diff)
parent2439066ad6901ed1e083f48fb7ac4fd7a7840d27 (diff)
Merge branch 'hypergraph-conversion'
Diffstat (limited to 'Data/Hypergraph/Base.agda')
-rw-r--r--Data/Hypergraph/Base.agda26
1 files changed, 26 insertions, 0 deletions
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
new file mode 100644
index 0000000..6988cf0
--- /dev/null
+++ b/Data/Hypergraph/Base.agda
@@ -0,0 +1,26 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Base (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Edge HL using (Edge; decTotalOrder; showEdge)
+open import Data.List.Base using (List; map)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String; unlines)
+
+import Data.List.Sort as Sort
+
+record Hypergraph (v : ℕ) : Set where
+ constructor mkHypergraph
+ field
+ edges : List (Edge v)
+
+sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
+sortHypergraph {v} H = record { edges = sort edges }
+ where
+ open Hypergraph H
+ open Sort decTotalOrder using (sort)
+
+showHypergraph : {v : ℕ} → Hypergraph v → String
+showHypergraph record { edges = e} = unlines (map showEdge e)