summaryrefslogtreecommitdiff
path: root/src/Cfe/Language
diff options
context:
space:
mode:
Diffstat (limited to 'src/Cfe/Language')
-rw-r--r--src/Cfe/Language/Construct/Concatenate.agda7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index ef45432..428e8a4 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -26,10 +26,11 @@ module _
(B : Language b)
where
- module A = Language A
- module B = Language B
+ private
+ module A = Language A
+ module B = Language B
- infix 4 _∙_
+ infix 7 _∙_
Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l