From 4452303b5d1cf1843d006603a362e513ffb46e1f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 20 Oct 2023 09:36:35 +0100 Subject: [PATCH] fixed typo --- src/Data/Nat/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index e304ed659f..37b1f33ee0 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -2342,6 +2342,6 @@ open Data.Nat.Base public <-transˡ = <-≤-trans {-# WARNING_ON_USAGE <-transˡ -"Warning: <-transˡ was deprecated in v2.0. Please use ≤-<-trans instead. " +"Warning: <-transˡ was deprecated in v2.0. Please use <-≤-trans instead. " #-}