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/Axiomatic | |
| parent | 23e8afe152a84551491594aea133488523525410 (diff) | |
Add more properties for ordered structures.
Diffstat (limited to 'src/Helium/Semantics/Axiomatic')
| -rw-r--r-- | src/Helium/Semantics/Axiomatic/Term.agda | 4 |
1 files changed, 2 insertions, 2 deletions
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 |