From 0fb884eb07bbea2f9e7d77b1df2af5794b989d74 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Apr 2024 11:43:49 -0700 Subject: [PATCH] Use implicit arguments for more things Signed-off-by: Danila Fedorin --- Language/Properties.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Language/Properties.agda b/Language/Properties.agda index 9446b42..2fb870e 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -32,27 +32,27 @@ buildCfg-output (if _ then s₁ else s₂) = (_ , refl) buildCfg-output (while _ repeat s) with (idx , p) ← buildCfg-output s rewrite p = (_ , refl) -Trace-∙ˡ : ∀ (g₁ g₂ : Graph) {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} → +Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} → Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ → Trace {g₁ ∙ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂ -Trace-∙ˡ g₁ g₂ {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) +Trace-∙ˡ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) = Trace-single ρ₁⇒ρ₂ -Trace-∙ˡ g₁ g₂ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') +Trace-∙ˡ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) = Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (_↑ˡ Graph.size g₂) idx₁→idx)) - (Trace-∙ˡ g₁ g₂ tr') + (Trace-∙ˡ tr') -Trace-∙ʳ : ∀ (g₁ g₂ : Graph) {idx₁ idx₂ : Graph.Index g₂} {ρ₁ ρ₂ : Env} → +Trace-∙ʳ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₂} {ρ₁ ρ₂ : Env} → Trace {g₂} idx₁ idx₂ ρ₁ ρ₂ → Trace {g₁ ∙ g₂} (Graph.size g₁ Fin.↑ʳ idx₁) (Graph.size g₁ Fin.↑ʳ idx₂) ρ₁ ρ₂ -Trace-∙ʳ g₁ g₂ {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) +Trace-∙ʳ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) = Trace-single ρ₁⇒ρ₂ -Trace-∙ʳ g₁ g₂ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') +Trace-∙ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) = Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ _ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx)) - (Trace-∙ʳ g₁ g₂ tr') + (Trace-∙ʳ tr') Trace-↦ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} → Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →