diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NBase.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index e90977e3d..eb46e69de 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -25,12 +25,12 @@ only one time. *) Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. (* Here we probably need to re-prove all axioms declared in NAxioms.v to -make sure that the definitions like N, S and plus are unfolded in them, +make sure that the definitions like N, S and add are unfolded in them, since unfolding is done only inside a functor. In fact, we'll do it in the files that prove the corresponding properties. In those files, we will also rename properties proved in NZ files by removing NZ from their names. In this way, one only has to consult, for example, NPlus.v to see all -available properties for plus, i.e., one does not have to go to NAxioms.v +available properties for add, i.e., one does not have to go to NAxioms.v for axioms and NZPlus.v for theorems. *) Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2. |