Somewhat better naming

0xd34df00d · Jan 1, 2021 · 335692e · 335692e
1 parent b40a4c0
commit 335692e
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/agda/Surface/Operational/BetaEquivalence.agda b/agda/Surface/Operational/BetaEquivalence.agda
@@ -72,9 +72,9 @@ data _≡rβ'_ : SType ℓ → SType ℓ → Set where
             → τ₁ ≡rβ  τ₂
 ≡rβ'-to-≡rβ (≡rβ'-Subst ε ε' τ ε↝ε' refl refl) = ≡rβ-Subst ε ε' τ ε↝ε'
 
-≡rβ-⇔-≡rβ' : (τ₁ ≡rβ' τ₂ → τ₁' ≡rβ'  τ₂')
-           → (τ₁ ≡rβ  τ₂ → τ₁' ≡rβ   τ₂')
-≡rβ-⇔-≡rβ' f = ≡rβ'-to-≡rβ ∘ f ∘ ≡rβ-to-≡rβ'
+prove-via-≡rβ' : (τ₁ ≡rβ' τ₂ → τ₁' ≡rβ'  τ₂')
+               → (τ₁ ≡rβ  τ₂ → τ₁' ≡rβ   τ₂')
+prove-via-≡rβ' f = ≡rβ'-to-≡rβ ∘ f ∘ ≡rβ-to-≡rβ'
 
 
 ≡rβ'-preserves-shape : ShapePreserving {ℓ} _≡rβ'_
@@ -126,4 +126,4 @@ data _≡rβ'_ : SType ℓ → SType ℓ → Set where
            → (idx : Fin (suc n))
            → (⊍ cons₁) ≡rβ (⊍ cons₂)
            → lookup cons₁ idx ≡rβ lookup cons₂ idx
-≡rβ-lookup idx = ≡rβ-⇔-≡rβ' (≡rβ'-lookup idx _ _)
+≡rβ-lookup idx = prove-via-≡rβ' (≡rβ'-lookup idx _ _)