Removal of Data.Nat.Properties.Simple in v1.0 of the standard library
Opened this issue · 1 comments
MatthewDaggitt commented
Hi, this is a ping that the module Data.Nat.Properties.Simple
will be removed in the upcoming release of v1.0 the standard library. The module has been deprecated since v0.14.
If you wish to continue using the latest version of the standard library you will need to update some of the files.
This can be done by replacing open import Data.Nat.Properties.Simple
with open import Data.Nat.Properties
.
JacquesCarette commented
Thanks!