From 96f3ceaeb291b1cea14fea5790d0af4607f8344e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 10 Mar 2024 19:41:02 -0700 Subject: [PATCH] Use the previous join function directly in GeneralizedUpdate Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 42ed8ad..672976b 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -204,7 +204,7 @@ module _ (prog : Program) where in vs updatingᵛ (k ∷ []) via (λ _ → eval e k∈e⇒k∈vars vs) - open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateForState {!!} states + open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ joinAll (λ {a₁} {a₂} a₁≼a₂ → joinAll-Mono {a₁} {a₂} a₁≼a₂) updateForState {!!} states renaming ( f' to updateAll ; f'-Monotonic to updateAll-Mono