From 4b0541caf58bd83eaf0b58870dbf30b2504b0bcd Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Dec 2025 14:06:28 -0800 Subject: [PATCH] Use "top" instead of T Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 39ea18e..fc4b450 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -371,8 +371,8 @@ record Graph : Set where Has-⊤ : Set Has-⊤ = Any Is-⊤ (proj₁ nodes) - Has-T? : Dec Has-⊤ - Has-T? = findUniversal (proj₁ nodes) PathExists? + Has-⊤? : Dec Has-⊤ + Has-⊤? = findUniversal (proj₁ nodes) PathExists? Has-⊥ : Set Has-⊥ = Any Is-⊥ (proj₁ nodes)