Skip to content

Commit 8f5de04

Browse files
committed
[fix] issue #1865 for Data.Nat
1 parent aebe3e7 commit 8f5de04

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/Data/Nat/Properties.agda

+4
Original file line numberDiff line numberDiff line change
@@ -2289,3 +2289,7 @@ suc[pred[n]]≡n {suc n} _ = refl
22892289
{-# WARNING_ON_USAGE <-step
22902290
"Warning: <-step was deprecated in v2.0. Please use m<n⇒m<1+n instead. "
22912291
#-}
2292+
2293+
{- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
2294+
open Data.Nat.Base public
2295+
using (*-rawMagma; *-1-rawMonoid)

0 commit comments

Comments
 (0)