diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-02 11:41:51 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-02 11:59:21 +0100 |
| commit | 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c (patch) | |
| tree | d9422bd08ee318b3fad90d03210f6a02a4c30783 /src/Helium/Semantics/Denotational/Core.agda | |
| parent | 23e8afe152a84551491594aea133488523525410 (diff) | |
Add more properties for ordered structures.
Diffstat (limited to 'src/Helium/Semantics/Denotational/Core.agda')
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 090e0ba..07c71bd 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -33,7 +33,7 @@ import Induction as I import Induction.WellFounded as Wf open import Level using (Level; _⊔_; 0ℓ) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) -open import Relation.Nullary using (does) +open import Relation.Nullary using (does) renaming (¬_ to ¬′_) open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness) ⟦_⟧ₗ : Type → Level @@ -196,12 +196,12 @@ pow : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ pow int x n = x ℤ′.^′ n pow real x n = x ℝ′.^′ n -shiftr : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ +shiftr : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ shiftr 2≉0 x n = ⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋ module Expression {o} {Σ : Vec Type o} - (2≉0 : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ) + (2≉0 : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where open Code Σ |