diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-05 12:06:33 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-04-05 12:06:33 +0100 |
| commit | b212c150ec0a9bf45cf6c28fba997693669e78d2 (patch) | |
| tree | 65351de7452c7e9fd111354d185e10c94eb4c569 /src/Helium/Data/Pseudocode | |
| parent | 6acd0e87fa8ab2a3230626b37f1cd02181810a1a (diff) | |
Minor clean up.
Diffstat (limited to 'src/Helium/Data/Pseudocode')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Algebra/Properties.agda | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda index 1c52cda..39bd1e7 100644 --- a/src/Helium/Data/Pseudocode/Algebra/Properties.agda +++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda @@ -238,11 +238,6 @@ module ⌊⌋ where ⌊ x ⌋ ℤ.+ ⌊ y ⌋ ℤ.+ 1ℤ ∎ where open ℤ.Reasoning - -- ⌊⌊x⌋+m/n⌋≈⌊x+m/n⌋ : ∀ x m {n} → (n>0 : n ℤ.> 0) → - -- let n≉0 = ℤ.<⇒≉ n>0 ∘ ℤ.Eq.sym in - -- ⌊ ⌊ x ⌋ /1 ℝ.* m /1 ℝ.* n≉0 ℤ.⁻¹ ⌋ ℤ.≈ ⌊ x ℝ.* m /1 ℝ.* n≉0 ℤ.⁻¹ ⌋ - -- ⌊⌊x⌋+m/n⌋≈⌊x+m/n⌋ x m {n} n>0 = ℤ.≤∧≮⇒≈ {!!} {!!} - f-monocont+int-preimage⇒⌊f⌊x⌋⌋≈⌊fx⌋ : ∀ (f : ℝ → ℝ) → ℝ.IsMonotoneContinuous f → ℝ.IntegerPreimage f → ∀ x → ⌊ f (⌊ x ⌋ /1) ⌋ ℤ.≈ ⌊ f x ⌋ |