From 87a3d6bda18470649eedd7da40cc6bcdc4c588b3 Mon Sep 17 00:00:00 2001 From: Junyoung/Clare Jang Date: Sat, 15 Mar 2025 18:09:11 -0400 Subject: [PATCH] Match on _IsRelatedTo_ later --- src/Relation/Binary/Reasoning/Base/Partial.agda | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda index 5da6792f64..9917a00d52 100644 --- a/src/Relation/Binary/Reasoning/Base/Partial.agda +++ b/src/Relation/Binary/Reasoning/Base/Partial.agda @@ -31,9 +31,12 @@ data _IsRelatedTo_ : A → A → Set (a ⊔ ℓ) where singleStep : ∀ x → x IsRelatedTo x multiStep : ∀ {x y} (x∼y : x ∼ y) → x IsRelatedTo y +∼-go-build : Trans _∼_ _IsRelatedTo_ _∼_ +∼-go-build x∼y (singleStep y) = x∼y +∼-go-build x∼y (multiStep y∼z) = trans x∼y y∼z + ∼-go : Trans _∼_ _IsRelatedTo_ _IsRelatedTo_ -∼-go x∼y (singleStep y) = multiStep x∼y -∼-go x∼y (multiStep y∼z) = multiStep (trans x∼y y∼z) +∼-go x∼y y