From 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 2 Apr 2022 11:41:51 +0100 Subject: Add more properties for ordered structures. --- src/Helium/Semantics/Denotational/Core.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Helium/Semantics/Denotational') 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 Σ -- cgit v1.2.3