summaryrefslogtreecommitdiff
path: root/src/Cfe/Language/Base.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Cfe/Language/Base.agda')
-rw-r--r--src/Cfe/Language/Base.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index bda9000..3e954b2 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -68,4 +68,4 @@ first : ∀ {a} → Language a → C → Set (c ⊔ a)
first A x = ∃[ l ] x ∷ l ∈ A
flast : ∀ {a} → Language a → C → Set (c ⊔ a)
-flast A x = ∃[ l ] (l ≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
+flast A x = ∃[ l ] (l ≢ [] × l ∈ A × ∃[ l′ ] l ++ x ∷ l′ ∈ A)