From a9b3af387a0a43ff5e21dcddb4ea7aa41f9baebc Mon Sep 17 00:00:00 2001 From: = Date: Sun, 22 Sep 2019 10:50:01 +0800 Subject: [PATCH] Fixed deprecation warnings in `Data.Bin.Properties` --- src/Data/Bin/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Bin/Properties.agda b/src/Data/Bin/Properties.agda index 496105a49c..a82ff356f1 100644 --- a/src/Data/Bin/Properties.agda +++ b/src/Data/Bin/Properties.agda @@ -77,7 +77,7 @@ as 1# ≟ bs 1# with as ≟ₑ bs 1+ (m₁ +ℕ n₁ *ℕ 2) ≤⟨ s≤s (ℕₚ.+-monoˡ-≤ _ (𝔽ₚ.toℕ≤pred[n] a)) ⟩ 1+ (1 +ℕ n₁ *ℕ 2) ≡⟨ refl ⟩ 1+ n₁ *ℕ 2 ≤⟨ ℕₚ.*-mono-≤ lt ℕₚ.≤-refl ⟩ - n₂ *ℕ 2 ≤⟨ ℕₚ.n≤m+n m₂ (n₂ *ℕ 2) ⟩ + n₂ *ℕ 2 ≤⟨ ℕₚ.m≤n+m (n₂ *ℕ 2) m₂ ⟩ m₂ +ℕ n₂ *ℕ 2 ∎) where open ℕₚ.≤-Reasoning @@ -94,7 +94,7 @@ as 1# ≟ bs 1# with as ≟ₑ bs m₁ = Fin.toℕ a; m₂ = Fin.toℕ b; n = toℕ (bs 1#) 1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1# -1<[23] {b} = less (ℕₚ.n≤m+n (Fin.toℕ b) 2) +1<[23] {b} = less (ℕₚ.m≤n+m 2 (Fin.toℕ b)) 1<2+ : ∀ {b bs} → [] 1# < (b ∷ bs) 1# 1<2+ {_} {[]} = 1<[23]