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

Use "top" instead of T

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2025-12-23 14:06:28 -08:00
parent 299938d97e
commit 4b0541caf5
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
Lattice/Builder.agda
View File

@@ -371,8 +371,8 @@ record Graph : Set where
Has-⊤ : Set Has-⊤ : Set
Has-⊤ = Any Is-⊤ (proj₁ nodes) Has-⊤ = Any Is-⊤ (proj₁ nodes)
Has-T? : Dec Has-⊤ Has-⊤? : Dec Has-⊤
Has-T? = findUniversal (proj₁ nodes) PathExists? Has-⊤? = findUniversal (proj₁ nodes) PathExists?
Has-⊥ : Set Has-⊥ : Set
Has-⊥ = Any Is-⊥ (proj₁ nodes) Has-⊥ = Any Is-⊥ (proj₁ nodes)