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/Axiomatic/Term.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Helium/Semantics/Axiomatic') diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda index eaefb89..c9ddd02 100644 --- a/src/Helium/Semantics/Axiomatic/Term.agda +++ b/src/Helium/Semantics/Axiomatic/Term.agda @@ -32,7 +32,7 @@ import Helium.Data.Pseudocode.Manipulate as M open import Helium.Semantics.Axiomatic.Core rawPseudocode open import Level using (_⊔_; lift; lower) open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst) -open import Relation.Nullary using (does; yes; no) +open import Relation.Nullary using (¬_; does; yes; no) open import Relation.Nullary.Decidable.Core using (True; toWitness) open import Relation.Nullary.Negation using (contradiction) @@ -216,7 +216,7 @@ cast τ eq = func₁ (cast′ τ eq) [ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t 2≉0 : Set _ -2≉0 = 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ +2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ [_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int [ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t -- cgit v1.2.3