diff options
Diffstat (limited to 'src/Cfe/Language/Base.agda')
| -rw-r--r-- | src/Cfe/Language/Base.agda | 2 |
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) |