diff options
| -rw-r--r-- | src/Cfe/Language/Base.agda | 2 | ||||
| -rw-r--r-- | src/Cfe/Language/Properties.agda | 21 |
2 files changed, 22 insertions, 1 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index eeea11d..2e77b11 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -46,4 +46,4 @@ fix : (Language → Language) → Language fix f l = ∃[ n ] iterate f n ∅ l _≤_ : Language → Language → Set (a ⊔ ℓ) -A ≤ B = ∀ l → A l → B l +A ≤ B = ∀ {l} → A l → B l diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda new file mode 100644 index 0000000..8d024a8 --- /dev/null +++ b/src/Cfe/Language/Properties.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary + +module Cfe.Language.Properties + {a ℓ} (setoid : Setoid a ℓ) + where + +open Setoid setoid renaming (Carrier to A) + +open import Cfe.Language setoid +open import Function + +------------------------------------------------------------------------ +-- Properties of _≤_ + +≤-refl : Reflexive _≤_ +≤-refl = id + +≤-trans : Transitive _≤_ +≤-trans A≤B B≤C = B≤C ∘ A≤B |