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.agda | |
| parent | 23e8afe152a84551491594aea133488523525410 (diff) | |
Add more properties for ordered structures.
Diffstat (limited to 'src/Helium/Semantics/Axiomatic.agda')
| -rw-r--r-- | src/Helium/Semantics/Axiomatic.agda | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/src/Helium/Semantics/Axiomatic.agda b/src/Helium/Semantics/Axiomatic.agda index dfac609..2fa3db1 100644 --- a/src/Helium/Semantics/Axiomatic.agda +++ b/src/Helium/Semantics/Axiomatic.agda @@ -15,11 +15,10 @@ module Helium.Semantics.Axiomatic open import Helium.Data.Pseudocode.Algebra.Properties pseudocode -open import Agda.Builtin.FromNat open import Data.Nat using (ℕ) -import Data.Nat.Literals as ℕₗ import Data.Unit open import Data.Vec using (Vec) +open import Function using (_∘_) open import Helium.Data.Pseudocode.Core import Helium.Semantics.Axiomatic.Core rawPseudocode as Core import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion @@ -36,12 +35,8 @@ open Term.Term public open Term public using (Term) -instance - numberℕ : Number ℕ - numberℕ = ℕₗ.number - -2≉0 : 2 ℝ.≉ 0 -2≉0 = ℝ.>⇒≉ (ℝ.n≉0⇒0<+n 2) +2≉0 : 2 ℝ.× 1ℝ ℝ.≉ 0ℝ +2≉0 = ℝ.<⇒≉ (ℝ.n≢0∧x>0⇒n×x>0 2 (ℝ.≤∧≉⇒< ℝ.0≤1 (ℝ.1≉0 ∘ ℝ.Eq.sym))) ∘ ℝ.Eq.sym HoareTriple : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} → Assertion Σ Γ Δ → Code.Statement Σ Γ → Assertion Σ Γ Δ → Set _ HoareTriple = Triple.HoareTriple 2≉0 |