search

JacquesCarette / TheoriesAndDataStructures

Showing how some simple mathematical theories naturally give rise to some common data-structures
38 stars 2 forks source link

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

Open MatthewDaggitt opened 5 years ago

MatthewDaggitt commented 5 years ago

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.

JacquesCarette commented 5 years ago

Thanks, we'll fix at least the parts outside Experiments that we want to keep!