From ad4592d4d2ef9a9b32a29d28dc6ba7273d3e8e0e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 21:34:17 -0700 Subject: [PATCH] Switch to using implicit arguments where needed Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index b161c25..4de15fb 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -215,9 +215,9 @@ module WithProg (prog : Program) where module WithValidity (interpretationValidˡ : InterpretationValid) where - updateVariablesFromStmt-matches : ∀ bs vs ρ₁ ρ₂ → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂ - updateVariablesFromStmt-matches _ vs ρ₁ ρ₁ (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁ - updateVariablesFromStmt-matches _ vs ρ₁ _ (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂ + updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂ + updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁ + updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂ with k ≟ˢ k' | k',v'∈ρ₂ ... | yes refl | here _ v _ rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =