diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-28 17:20:33 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-28 17:20:33 -0500 |
| commit | 0bf55c23ad3bee621d0e7425f5a5e875254e3450 (patch) | |
| tree | ea5dbac95aa1fa9449b785cb5be3078790a88aea /Data/Hypergraph/Base.agda | |
| parent | 2cd74f160389fe2ab2b30ab628fbb9b712f06faf (diff) | |
| parent | 2439066ad6901ed1e083f48fb7ac4fd7a7840d27 (diff) | |
Merge branch 'hypergraph-conversion'
Diffstat (limited to 'Data/Hypergraph/Base.agda')
| -rw-r--r-- | Data/Hypergraph/Base.agda | 26 |
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) |
