diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-03-21 16:50:55 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-03-21 16:50:55 +0000 |
| commit | 23e8afe152a84551491594aea133488523525410 (patch) | |
| tree | a8480eddd05459bb794679df6116e14182df0f43 /src/Helium/Semantics/Axiomatic | |
| parent | 5202560ea008a76048587f6ab63797f7517fbdc0 (diff) | |
Add all-in-one import for Hoare logic semantics.
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 57dad92..eaefb89 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 |