From baece236d34d568099d7ace8e492a5e2d19cc69d Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 28 Nov 2025 17:09:14 -0800
Subject: [PATCH] Re-define 'interior'

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 5 +++++
 1 file changed, 5 insertions(+)

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₂)