diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 16c57b8..ea3802d 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -47,6 +47,11 @@ record Graph : Set where done ++ p = p (step e p₁) ++ p₂ = step e (p₁ ++ p₂) + interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node + interior done = [] + interior (step _ done) = [] + interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p + Adjacency : Set Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)