diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-25 18:01:19 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-25 18:01:19 +0000 |
| commit | ba7e3b5d9c868af4b5dd7c3af72c48a1dd27cc31 (patch) | |
| tree | 42e9ec97d50edfd46afeb920260b1dc29058696f /src/Cfe/Language/Base.agda | |
| parent | abe9461e0dc194c160d97fee23a1646097a0c264 (diff) | |
Prove sequential unique decomposition.
Fix faulty definition of flast set.
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) |