DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Slightly help along implicit inference by moving binary less-than

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-01-05 19:12:34 -08:00
parent 236c92a5ef
commit 105321971f
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Analysis/Utils.agda Normal file
View File

@ -0,0 +1,15 @@
module Analysis.Utils where
open import Data.Product using (_,_)
open import Lattice
module _ {o} {O : Set o} {_≼ᴼ_ : O → O → Set o}
(≼ᴼ-trans : ∀ {o₁ o₂ o₃} → o₁ ≼ᴼ o₂ → o₂ ≼ᴼ o₃ → o₁ ≼ᴼ o₃)
(combine : O → O → O) (combine-Mono₂ : Monotonic₂ _≼ᴼ_ _≼ᴼ_ _≼ᴼ_ combine) where
eval-combine₂ : {o₁ o₂ o₃ o₄ : O} → o₁ ≼ᴼ o₃ → o₂ ≼ᴼ o₄ →
combine o₁ o₂ ≼ᴼ combine o₃ o₄
eval-combine₂ {o₁} {o₂} {o₃} {o₄} o₁≼o₃ o₂≼o₄ =
let (combine-Monoˡ , combine-Monoʳ) = combine-Mono₂
in ≼ᴼ-trans (combine-Monoˡ o₂ o₁≼o₃)
(combine-Monoʳ o₃ o₂≼o₄)