DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Re-define 'interior'

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-11-28 17:09:14 -08:00
parent 6f642d85e0
commit baece236d3
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Lattice/Builder.agda
View File

@ -47,6 +47,11 @@ record Graph : Set where
done ++ p = p done ++ p = p
(step e p₁) ++ p₂ = step e (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 : Set
Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂) Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)