Skip to content

The removal of Data.Nat.Properties.Simple in v1.0 of the standard library #1

@MatthewDaggitt

Description

@MatthewDaggitt

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 the following files:

Helpers/LeqLemmas.agda
Helpers/FinNatLemmas.agda
Helpers/FinEquivPlusTimes.agda
Structures/Experiments/Sidequest/Permutations/PermutationSequences.lagda
Structures/Experiments/Sidequest/Permutations/Vector.lagda
Structures/Experiments/VectorLemmas.agda
Structures/Experiments/Sidequest.lagda
Structures/Experiments/Sidequest/Permutations/SME.lagda

This can be done by replacing open import Data.Nat.Properties.Simple with open import Data.Nat.Properties.

Metadata

Metadata

Labels

No labels
No labels

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions