From 105321971f4fbb6a82c0df15ee1b2139add186db Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 5 Jan 2025 19:12:34 -0800 Subject: [PATCH] Slightly help along implicit inference by moving binary less-than Signed-off-by: Danila Fedorin --- Analysis/Utils.agda | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 Analysis/Utils.agda diff --git a/Analysis/Utils.agda b/Analysis/Utils.agda new file mode 100644 index 0000000..b87a3c8 --- /dev/null +++ b/Analysis/Utils.agda @@ -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₄)