From bce3e4dd0e4ed624667a273becff1bdae3d63ef6 Mon Sep 17 00:00:00 2001 From: Github Actions Date: Thu, 2 Jan 2025 15:34:28 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-stdlib@d481f5c5bbd3c3a607572558e7ad104642cc9d8c=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- master/Data.List.Relation.Binary.Equality.Setoid.html | 8 ++++---- master/Data.List.Relation.Binary.Pointwise.html | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/master/Data.List.Relation.Binary.Equality.Setoid.html b/master/Data.List.Relation.Binary.Equality.Setoid.html index 5aad7fe21a..414e211232 100644 --- a/master/Data.List.Relation.Binary.Equality.Setoid.html +++ b/master/Data.List.Relation.Binary.Equality.Setoid.html @@ -112,11 +112,11 @@ ++⁺ : ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs ++⁺ = PW.++⁺ -++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs -++⁺ʳ xs = PW.++⁺ʳ refl xs +++⁺ˡ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs +++⁺ˡ xs = PW.++⁺ˡ refl xs -++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs -++⁺ˡ zs = PW.++⁺ˡ refl zs +++⁺ʳ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs +++⁺ʳ zs = PW.++⁺ʳ refl zs ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs ++-cancelˡ xs = PW.++-cancelˡ xs diff --git a/master/Data.List.Relation.Binary.Pointwise.html b/master/Data.List.Relation.Binary.Pointwise.html index 887f8f69f4..21f3cac66e 100644 --- a/master/Data.List.Relation.Binary.Pointwise.html +++ b/master/Data.List.Relation.Binary.Pointwise.html @@ -169,11 +169,11 @@ module _ (rfl : Reflexive R) where - ++⁺ʳ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) - ++⁺ʳ xs = ++⁺ (refl rfl) + ++⁺ˡ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) + ++⁺ˡ xs = ++⁺ (refl rfl) - ++⁺ˡ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) - ++⁺ˡ zs rs = ++⁺ rs (refl rfl) + ++⁺ʳ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) + ++⁺ʳ zs rs = ++⁺ rs (refl rfl) ------------------------------------------------------------------------