From 8fe59242449d8078b5ff32f9cd18e7533c521077 Mon Sep 17 00:00:00 2001 From: coqbot Date: Fri, 24 Jan 2025 10:43:26 +0000 Subject: [PATCH] =?UTF-8?q?Documentation=20of=20branch=20=E2=80=9Cv9.0?= =?UTF-8?q?=E2=80=9D=20at=207664abca?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- v9.0/corelib/html/Corelib.BinNums.IntDef.html | 34 +++--- v9.0/corelib/html/Corelib.BinNums.NatDef.html | 8 +- v9.0/corelib/html/Corelib.BinNums.PosDef.html | 40 +++---- .../html/Corelib.Classes.CMorphisms.html | 4 +- .../Corelib.Classes.CRelationClasses.html | 6 +- .../html/Corelib.Classes.Equivalence.html | 2 +- v9.0/corelib/html/Corelib.Classes.Init.html | 2 +- .../html/Corelib.Classes.Morphisms.html | 4 +- .../html/Corelib.Classes.Morphisms_Prop.html | 2 +- .../html/Corelib.Classes.RelationClasses.html | 6 +- .../html/Corelib.Classes.SetoidTactics.html | 2 +- .../html/Corelib.Floats.FloatAxioms.html | 2 +- .../corelib/html/Corelib.Floats.FloatOps.html | 2 +- .../html/Corelib.Floats.PrimFloat.html | 22 ++-- .../html/Corelib.Floats.SpecFloat.html | 8 +- v9.0/corelib/html/Corelib.Init.Byte.html | 2 +- v9.0/corelib/html/Corelib.Init.Datatypes.html | 14 +-- v9.0/corelib/html/Corelib.Init.Decimal.html | 2 +- .../html/Corelib.Init.Hexadecimal.html | 2 +- v9.0/corelib/html/Corelib.Init.Logic.html | 8 +- v9.0/corelib/html/Corelib.Init.Nat.html | 28 ++--- v9.0/corelib/html/Corelib.Init.Number.html | 2 +- v9.0/corelib/html/Corelib.Init.Tactics.html | 4 +- v9.0/corelib/html/Corelib.Init.Tauto.html | 2 +- v9.0/corelib/html/Corelib.Init.Wf.html | 2 +- v9.0/corelib/html/Corelib.Lists.ListDef.html | 10 +- .../Corelib.Strings.PrimStringAxioms.html | 4 +- v9.0/corelib/html/index_global_T.html | 2 +- v9.0/corelib/html/index_global_W.html | 2 +- v9.0/corelib/html/index_library_T.html | 2 +- v9.0/corelib/html/index_library_W.html | 2 +- .../.doctrees/environment.pickle | Bin 68955 -> 68955 bytes .../.doctrees/language/coq-library.doctree | Bin 231125 -> 231125 bytes .../.doctrees/addendum/extraction.doctree | Bin 355364 -> 355364 bytes .../addendum/generalized-rewriting.doctree | Bin 866882 -> 866882 bytes .../.doctrees/addendum/micromega.doctree | Bin 398147 -> 398147 bytes .../refman/.doctrees/addendum/program.doctree | Bin 247075 -> 247075 bytes .../.doctrees/addendum/rewrite-rules.doctree | Bin 169832 -> 169832 bytes v9.0/refman/.doctrees/addendum/ring.doctree | Bin 684697 -> 684697 bytes .../addendum/universe-polymorphism.doctree | Bin 937449 -> 937449 bytes v9.0/refman/.doctrees/environment.pickle | Bin 856071 -> 856071 bytes .../.doctrees/language/coq-library.doctree | Bin 930322 -> 930322 bytes .../language/core/assumptions.doctree | Bin 187472 -> 187472 bytes .../.doctrees/language/core/basic.doctree | Bin 368741 -> 368741 bytes .../.doctrees/language/core/inductive.doctree | Bin 1245510 -> 1245510 bytes .../.doctrees/language/core/modules.doctree | Bin 650160 -> 650160 bytes .../.doctrees/language/core/primitive.doctree | Bin 166504 -> 166504 bytes .../extensions/arguments-command.doctree | Bin 552388 -> 552388 bytes .../language/extensions/evars.doctree | Bin 205100 -> 205100 bytes .../extensions/implicit-arguments.doctree | Bin 548954 -> 548954 bytes .../language/extensions/match.doctree | Bin 977499 -> 977499 bytes .../.doctrees/proof-engine/ltac.doctree | Bin 2087911 -> 2087911 bytes .../.doctrees/proof-engine/ltac2.doctree | Bin 1287801 -> 1287801 bytes .../ssreflect-proof-language.doctree | Bin 5544318 -> 5544318 bytes .../.doctrees/proof-engine/tactics.doctree | Bin 1587240 -> 1587240 bytes .../proof-engine/vernacular-commands.doctree | Bin 846476 -> 846476 bytes .../proofs/automatic-tactics/auto.doctree | Bin 567841 -> 567841 bytes .../proofs/writing-proofs/equality.doctree | Bin 890081 -> 890072 bytes .../proofs/writing-proofs/proof-mode.doctree | Bin 703744 -> 703744 bytes .../reasoning-inductives.doctree | Bin 1728725 -> 1728725 bytes .../user-extensions/syntax-extensions.doctree | Bin 2222751 -> 2222751 bytes .../.doctrees/using/libraries/funind.doctree | Bin 424925 -> 424925 bytes .../.doctrees/using/libraries/writing.doctree | Bin 123480 -> 123480 bytes v9.0/refman/proof-engine/ltac.html | 50 ++++---- .../proofs/writing-proofs/equality.html | 6 +- v9.0/refman/searchindex.js | 2 +- v9.0/stdlib/Stdlib.Arith.Arith_base.html | 4 +- v9.0/stdlib/Stdlib.Arith.EqNat.html | 2 +- v9.0/stdlib/Stdlib.Arith.PeanoNat.html | 30 ++--- v9.0/stdlib/Stdlib.Bool.Bool.html | 30 ++--- v9.0/stdlib/Stdlib.Bool.BoolOrder.html | 6 +- v9.0/stdlib/Stdlib.Classes.CEquivalence.html | 2 +- .../stdlib/Stdlib.Classes.DecidableClass.html | 2 +- v9.0/stdlib/Stdlib.Classes.EquivDec.html | 2 +- .../Stdlib.Classes.Morphisms_Relations.html | 2 +- v9.0/stdlib/Stdlib.Classes.RelationPairs.html | 2 +- v9.0/stdlib/Stdlib.Classes.SetoidClass.html | 2 +- v9.0/stdlib/Stdlib.Classes.SetoidDec.html | 2 +- v9.0/stdlib/Stdlib.FSets.FMapAVL.html | 90 +++++++------- v9.0/stdlib/Stdlib.FSets.FMapFacts.html | 36 +++--- v9.0/stdlib/Stdlib.FSets.FMapFullAVL.html | 26 ++--- v9.0/stdlib/Stdlib.FSets.FMapInterface.html | 12 +- v9.0/stdlib/Stdlib.FSets.FMapList.html | 24 ++-- v9.0/stdlib/Stdlib.FSets.FMapPositive.html | 2 +- v9.0/stdlib/Stdlib.FSets.FMapWeakList.html | 22 ++-- v9.0/stdlib/Stdlib.FSets.FSetAVL.html | 2 +- v9.0/stdlib/Stdlib.FSets.FSetBridge.html | 6 +- v9.0/stdlib/Stdlib.FSets.FSetCompat.html | 10 +- v9.0/stdlib/Stdlib.FSets.FSetDecide.html | 32 ++--- .../stdlib/Stdlib.FSets.FSetEqProperties.html | 2 +- v9.0/stdlib/Stdlib.FSets.FSetInterface.html | 16 +-- v9.0/stdlib/Stdlib.FSets.FSetList.html | 2 +- v9.0/stdlib/Stdlib.FSets.FSetProperties.html | 28 ++--- v9.0/stdlib/Stdlib.FSets.FSetToFiniteSet.html | 4 +- v9.0/stdlib/Stdlib.FSets.FSetWeakList.html | 2 +- v9.0/stdlib/Stdlib.Floats.FloatLemmas.html | 2 +- v9.0/stdlib/Stdlib.Lists.List.html | 64 +++++----- v9.0/stdlib/Stdlib.Lists.SetoidList.html | 2 +- v9.0/stdlib/Stdlib.Lists.StreamMemo.html | 2 +- v9.0/stdlib/Stdlib.Logic.ChoiceFacts.html | 58 ++++----- .../stdlib/Stdlib.Logic.ClassicalEpsilon.html | 2 +- v9.0/stdlib/Stdlib.Logic.ClassicalFacts.html | 28 ++--- v9.0/stdlib/Stdlib.Logic.Diaconescu.html | 6 +- v9.0/stdlib/Stdlib.Logic.EqdepFacts.html | 6 +- v9.0/stdlib/Stdlib.Logic.Eqdep_dec.html | 6 +- .../Stdlib.Logic.ExtensionalityFacts.html | 8 +- v9.0/stdlib/Stdlib.Logic.FinFun.html | 2 +- v9.0/stdlib/Stdlib.Logic.Hurkens.html | 76 ++++++------ .../Stdlib.Logic.PropExtensionalityFacts.html | 10 +- v9.0/stdlib/Stdlib.Logic.PropFacts.html | 2 +- v9.0/stdlib/Stdlib.Logic.SetIsType.html | 2 +- v9.0/stdlib/Stdlib.MSets.MSetAVL.html | 68 +++++------ v9.0/stdlib/Stdlib.MSets.MSetDecide.html | 32 ++--- .../stdlib/Stdlib.MSets.MSetEqProperties.html | 2 +- v9.0/stdlib/Stdlib.MSets.MSetFacts.html | 10 +- v9.0/stdlib/Stdlib.MSets.MSetGenTree.html | 54 ++++----- v9.0/stdlib/Stdlib.MSets.MSetInterface.html | 14 +-- v9.0/stdlib/Stdlib.MSets.MSetList.html | 10 +- v9.0/stdlib/Stdlib.MSets.MSetProperties.html | 28 ++--- v9.0/stdlib/Stdlib.MSets.MSetRBT.html | 84 ++++++------- v9.0/stdlib/Stdlib.MSets.MSetToFiniteSet.html | 4 +- v9.0/stdlib/Stdlib.MSets.MSetWeakList.html | 10 +- v9.0/stdlib/Stdlib.NArith.BinNat.html | 4 +- v9.0/stdlib/Stdlib.NArith.BinNatDef.html | 12 +- v9.0/stdlib/Stdlib.NArith.Nnat.html | 4 +- .../Stdlib.Numbers.AltBinNotations.html | 2 +- ....Numbers.Cyclic.Abstract.CyclicAxioms.html | 2 +- ...dlib.Numbers.Cyclic.Abstract.NZCyclic.html | 2 +- .../Stdlib.Numbers.Cyclic.Int63.Cyclic63.html | 2 +- .../Stdlib.Numbers.Cyclic.Int63.Ring63.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalFacts.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalN.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalNat.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalPos.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalQ.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalR.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalString.html | 2 +- v9.0/stdlib/Stdlib.Numbers.DecimalZ.html | 2 +- .../Stdlib.Numbers.HexadecimalFacts.html | 2 +- v9.0/stdlib/Stdlib.Numbers.HexadecimalN.html | 2 +- .../stdlib/Stdlib.Numbers.HexadecimalNat.html | 2 +- .../stdlib/Stdlib.Numbers.HexadecimalPos.html | 2 +- v9.0/stdlib/Stdlib.Numbers.HexadecimalQ.html | 2 +- v9.0/stdlib/Stdlib.Numbers.HexadecimalR.html | 2 +- .../Stdlib.Numbers.HexadecimalString.html | 2 +- v9.0/stdlib/Stdlib.Numbers.HexadecimalZ.html | 2 +- ...Stdlib.Numbers.Integer.Abstract.ZBits.html | 2 +- ...lib.Numbers.Integer.Abstract.ZDivEucl.html | 8 +- ...ib.Numbers.Integer.Abstract.ZDivFloor.html | 8 +- ...ib.Numbers.Integer.Abstract.ZDivTrunc.html | 8 +- .../Stdlib.Numbers.Integer.Abstract.ZLcm.html | 2 +- ...dlib.Numbers.Integer.Abstract.ZMaxMin.html | 2 +- ...Stdlib.Numbers.Integer.Binary.ZBinary.html | 2 +- v9.0/stdlib/Stdlib.Numbers.NaryFunctions.html | 2 +- v9.0/stdlib/Stdlib.Numbers.NatInt.NZAdd.html | 2 +- .../Stdlib.Numbers.NatInt.NZAddOrder.html | 2 +- .../Stdlib.Numbers.NatInt.NZAxioms.html | 10 +- v9.0/stdlib/Stdlib.Numbers.NatInt.NZBase.html | 2 +- v9.0/stdlib/Stdlib.Numbers.NatInt.NZDiv.html | 6 +- .../Stdlib.Numbers.NatInt.NZDomain.html | 6 +- v9.0/stdlib/Stdlib.Numbers.NatInt.NZLog.html | 2 +- v9.0/stdlib/Stdlib.Numbers.NatInt.NZMul.html | 2 +- .../Stdlib.Numbers.NatInt.NZMulOrder.html | 2 +- .../stdlib/Stdlib.Numbers.NatInt.NZOrder.html | 20 ++-- v9.0/stdlib/Stdlib.Numbers.NatInt.NZSqrt.html | 2 +- .../Stdlib.Numbers.Natural.Abstract.NDiv.html | 6 +- .../Stdlib.Numbers.Natural.Abstract.NLcm.html | 2 +- ...dlib.Numbers.Natural.Abstract.NMaxMin.html | 2 +- ...Stdlib.Numbers.Natural.Binary.NBinary.html | 2 +- v9.0/stdlib/Stdlib.PArith.BinPos.html | 110 +++++++++--------- v9.0/stdlib/Stdlib.PArith.BinPosDef.html | 22 ++-- v9.0/stdlib/Stdlib.PArith.POrderedType.html | 6 +- v9.0/stdlib/Stdlib.Program.Combinators.html | 2 +- v9.0/stdlib/Stdlib.QArith.QArith_base.html | 36 +++--- v9.0/stdlib/Stdlib.QArith.QOrderedType.html | 6 +- v9.0/stdlib/Stdlib.QArith.Qcabs.html | 2 +- v9.0/stdlib/Stdlib.QArith.Qfield.html | 2 +- v9.0/stdlib/Stdlib.QArith.Qminmax.html | 4 +- v9.0/stdlib/Stdlib.QArith.Qpower.html | 38 +++--- v9.0/stdlib/Stdlib.Reals.AltSeries.html | 6 +- ....Reals.Cauchy.ConstructiveCauchyReals.html | 2 +- ...ls.Cauchy.ConstructiveCauchyRealsMult.html | 2 +- v9.0/stdlib/Stdlib.Reals.Cauchy.QExtra.html | 10 +- .../Stdlib.Reals.ClassicalDedekindReals.html | 22 ++-- v9.0/stdlib/Stdlib.Reals.RIneq.html | 94 +++++++-------- v9.0/stdlib/Stdlib.Reals.ROrderedType.html | 6 +- v9.0/stdlib/Stdlib.Reals.R_Ifp.html | 4 +- v9.0/stdlib/Stdlib.Reals.R_sqrt.html | 4 +- v9.0/stdlib/Stdlib.Reals.Ranalysis1.html | 30 ++--- v9.0/stdlib/Stdlib.Reals.Ranalysis5.html | 12 +- v9.0/stdlib/Stdlib.Reals.Ratan.html | 50 ++++---- v9.0/stdlib/Stdlib.Reals.Raxioms.html | 18 +-- v9.0/stdlib/Stdlib.Reals.Rbasic_fun.html | 6 +- v9.0/stdlib/Stdlib.Reals.Rdefinitions.html | 4 +- v9.0/stdlib/Stdlib.Reals.Rfunctions.html | 14 +-- v9.0/stdlib/Stdlib.Reals.Rgeom.html | 8 +- v9.0/stdlib/Stdlib.Reals.RiemannInt_SF.html | 10 +- v9.0/stdlib/Stdlib.Reals.Rlimit.html | 10 +- v9.0/stdlib/Stdlib.Reals.Rlogic.html | 6 +- v9.0/stdlib/Stdlib.Reals.Rminmax.html | 4 +- v9.0/stdlib/Stdlib.Reals.Rpower.html | 10 +- v9.0/stdlib/Stdlib.Reals.Rseries.html | 4 +- v9.0/stdlib/Stdlib.Reals.Rtopology.html | 6 +- v9.0/stdlib/Stdlib.Reals.Rtrigo1.html | 6 +- v9.0/stdlib/Stdlib.Reals.Rtrigo_def.html | 6 +- v9.0/stdlib/Stdlib.Reals.Rtrigo_facts.html | 12 +- ...Stdlib.Relations.Operators_Properties.html | 8 +- .../Stdlib.Relations.Relation_Operators.html | 38 +++--- v9.0/stdlib/Stdlib.Sorting.CPermutation.html | 2 +- v9.0/stdlib/Stdlib.Sorting.Heap.html | 20 ++-- v9.0/stdlib/Stdlib.Sorting.PermutSetoid.html | 6 +- v9.0/stdlib/Stdlib.Sorting.Permutation.html | 2 +- v9.0/stdlib/Stdlib.Strings.Ascii.html | 6 +- v9.0/stdlib/Stdlib.Strings.PString.html | 14 +-- v9.0/stdlib/Stdlib.Strings.String.html | 16 +-- .../Stdlib.Structures.DecidableType.html | 6 +- .../Stdlib.Structures.DecidableTypeEx.html | 2 +- v9.0/stdlib/Stdlib.Structures.Equalities.html | 18 +-- .../Stdlib.Structures.EqualitiesFacts.html | 4 +- .../Stdlib.Structures.GenericMinMax.html | 18 +-- .../stdlib/Stdlib.Structures.OrderedType.html | 4 +- .../Stdlib.Structures.OrderedTypeAlt.html | 2 +- .../Stdlib.Structures.OrderedTypeEx.html | 2 +- v9.0/stdlib/Stdlib.Structures.Orders.html | 14 +-- v9.0/stdlib/Stdlib.Structures.OrdersAlt.html | 12 +- v9.0/stdlib/Stdlib.Structures.OrdersEx.html | 2 +- .../stdlib/Stdlib.Structures.OrdersFacts.html | 12 +- .../stdlib/Stdlib.Structures.OrdersLists.html | 4 +- v9.0/stdlib/Stdlib.Structures.OrdersTac.html | 8 +- v9.0/stdlib/Stdlib.Vectors.VectorDef.html | 4 +- v9.0/stdlib/Stdlib.Vectors.VectorSpec.html | 24 ++-- v9.0/stdlib/Stdlib.ZArith.BinInt.html | 80 ++++++------- v9.0/stdlib/Stdlib.ZArith.BinIntDef.html | 32 ++--- v9.0/stdlib/Stdlib.ZArith.Int.html | 8 +- v9.0/stdlib/Stdlib.ZArith.ZArith_dec.html | 4 +- v9.0/stdlib/Stdlib.ZArith.Zabs.html | 6 +- v9.0/stdlib/Stdlib.ZArith.Zbitwise.html | 8 +- v9.0/stdlib/Stdlib.ZArith.Zbool.html | 4 +- v9.0/stdlib/Stdlib.ZArith.Zcompare.html | 16 +-- v9.0/stdlib/Stdlib.ZArith.Zdiv.html | 18 +-- v9.0/stdlib/Stdlib.ZArith.Zeuclid.html | 2 +- v9.0/stdlib/Stdlib.ZArith.Zeven.html | 2 +- v9.0/stdlib/Stdlib.ZArith.Zgcd_alt.html | 2 +- v9.0/stdlib/Stdlib.ZArith.Zhints.html | 6 +- v9.0/stdlib/Stdlib.ZArith.Znat.html | 6 +- v9.0/stdlib/Stdlib.ZArith.Znumtheory.html | 10 +- v9.0/stdlib/Stdlib.ZArith.Zorder.html | 20 ++-- v9.0/stdlib/Stdlib.ZArith.Zpow_def.html | 2 +- v9.0/stdlib/Stdlib.ZArith.Zpow_facts.html | 4 +- v9.0/stdlib/Stdlib.ZArith.Zpower.html | 6 +- v9.0/stdlib/Stdlib.ZArith.Zquot.html | 10 +- v9.0/stdlib/Stdlib.ZArith.auxiliary.html | 2 +- v9.0/stdlib/Stdlib.btauto.Algebra.html | 4 +- .../Stdlib.extraction.ExtrHaskellNatInt.html | 6 +- ...dlib.extraction.ExtrHaskellNatInteger.html | 6 +- .../Stdlib.extraction.ExtrHaskellNatNum.html | 10 +- .../Stdlib.extraction.ExtrHaskellString.html | 12 +- .../Stdlib.extraction.ExtrHaskellZInt.html | 6 +- .../Stdlib.extraction.ExtrHaskellZNum.html | 10 +- v9.0/stdlib/Stdlib.omega.PreOmega.html | 2 +- v9.0/stdlib/index_global_T.html | 4 +- v9.0/stdlib/index_global_W.html | 2 +- v9.0/stdlib/index_library_T.html | 4 +- v9.0/stdlib/index_library_W.html | 2 +- 264 files changed, 1303 insertions(+), 1303 deletions(-) diff --git a/v9.0/corelib/html/Corelib.BinNums.IntDef.html b/v9.0/corelib/html/Corelib.BinNums.IntDef.html index 5a3dbf2b8c..dcb245d1cf 100644 --- a/v9.0/corelib/html/Corelib.BinNums.IntDef.html +++ b/v9.0/corelib/html/Corelib.BinNums.IntDef.html @@ -58,7 +58,7 @@

Library Corelib.BinNums.IntDef

-

Binary Integers, Definitions of Operations

+

Binary Integers, Definitions of Operations

@@ -73,7 +73,7 @@

Library Corelib.BinNums.IntDef

-

Doubling and variants

+

Doubling and variants

@@ -106,7 +106,7 @@

Library Corelib.BinNums.IntDef

-

Subtraction of positive into Z

+

Subtraction of positive into Z

@@ -129,7 +129,7 @@

Library Corelib.BinNums.IntDef

-

Addition

+

Addition

@@ -152,7 +152,7 @@

Library Corelib.BinNums.IntDef

-

Opposite

+

Opposite

@@ -172,7 +172,7 @@

Library Corelib.BinNums.IntDef

-

Subtraction

+

Subtraction

@@ -187,7 +187,7 @@

Library Corelib.BinNums.IntDef

-

Multiplication

+

Multiplication

@@ -210,7 +210,7 @@

Library Corelib.BinNums.IntDef

-

Power function

+

Power function

@@ -233,7 +233,7 @@

Library Corelib.BinNums.IntDef

-

Comparison

+

Comparison

@@ -302,7 +302,7 @@

Library Corelib.BinNums.IntDef

-

Minimum and maximum

+

Minimum and maximum

@@ -325,7 +325,7 @@

Library Corelib.BinNums.IntDef

-

Conversions

+

Conversions

@@ -389,11 +389,11 @@

Library Corelib.BinNums.IntDef

-

Euclidean divisions for binary integers

+

Euclidean divisions for binary integers

-

Floor division

+

Floor division

@@ -484,7 +484,7 @@

Library Corelib.BinNums.IntDef

-

Trunc Division

+

Trunc Division

@@ -545,7 +545,7 @@

Library Corelib.BinNums.IntDef

No infix notation for rem, otherwise it becomes a keyword
-

Parity functions

+

Parity functions

@@ -563,7 +563,7 @@

Library Corelib.BinNums.IntDef

-

Division by two

+

Division by two

@@ -586,7 +586,7 @@

Library Corelib.BinNums.IntDef

-

Square root

+

Square root

diff --git a/v9.0/corelib/html/Corelib.BinNums.NatDef.html b/v9.0/corelib/html/Corelib.BinNums.NatDef.html index 670b1dd02f..c3c53e35c8 100644 --- a/v9.0/corelib/html/Corelib.BinNums.NatDef.html +++ b/v9.0/corelib/html/Corelib.BinNums.NatDef.html @@ -52,7 +52,7 @@

Library Corelib.BinNums.NatDef

-

Binary natural numbers, definitions of operations

+

Binary natural numbers, definitions of operations

@@ -64,7 +64,7 @@

Library Corelib.BinNums.NatDef

-

Operation x -> 2*x+1

+

Operation x -> 2*x+1

@@ -80,7 +80,7 @@

Library Corelib.BinNums.NatDef

-

Operation x -> 2*x

+

Operation x -> 2*x

@@ -96,7 +96,7 @@

Library Corelib.BinNums.NatDef

-

The successor of a N can be seen as a positive

+

The successor of a N can be seen as a positive

diff --git a/v9.0/corelib/html/Corelib.BinNums.PosDef.html b/v9.0/corelib/html/Corelib.BinNums.PosDef.html index 2122076d86..cb0bc6d4e7 100644 --- a/v9.0/corelib/html/Corelib.BinNums.PosDef.html +++ b/v9.0/corelib/html/Corelib.BinNums.PosDef.html @@ -49,7 +49,7 @@

Library Corelib.BinNums.PosDef

-

Binary positive numbers, operations

+

Binary positive numbers, operations

@@ -97,11 +97,11 @@

Library Corelib.BinNums.PosDef

-

Operations over positive numbers

+

Operations over positive numbers

-

Successor

+

Successor

@@ -118,7 +118,7 @@

Library Corelib.BinNums.PosDef

-

Addition

+

Addition

@@ -154,7 +154,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x-1

+

Operation x -> 2*x-1

@@ -171,7 +171,7 @@

Library Corelib.BinNums.PosDef

-

The predecessor of a positive number can be seen as a N

+

The predecessor of a positive number can be seen as a N

@@ -188,7 +188,7 @@

Library Corelib.BinNums.PosDef

-

An auxiliary type for subtraction

+

An auxiliary type for subtraction

@@ -203,7 +203,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x+1

+

Operation x -> 2*x+1

@@ -220,7 +220,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x

+

Operation x -> 2*x

@@ -237,7 +237,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x-2

+

Operation x -> 2*x-2

@@ -254,7 +254,7 @@

Library Corelib.BinNums.PosDef

-

Subtraction, result as a mask

+

Subtraction, result as a mask

@@ -287,7 +287,7 @@

Library Corelib.BinNums.PosDef

-

Subtraction, result as a positive, returning 1 if x<=y

+

Subtraction, result as a positive, returning 1 if x<=y

@@ -303,7 +303,7 @@

Library Corelib.BinNums.PosDef

-

Multiplication

+

Multiplication

@@ -320,7 +320,7 @@

Library Corelib.BinNums.PosDef

-

Iteration over a positive number

+

Iteration over a positive number

@@ -337,7 +337,7 @@

Library Corelib.BinNums.PosDef

-

Division by 2 rounded below but for 1

+

Division by 2 rounded below but for 1

@@ -370,7 +370,7 @@

Library Corelib.BinNums.PosDef

-

Comparison on binary positive numbers

+

Comparison on binary positive numbers

@@ -396,7 +396,7 @@

Library Corelib.BinNums.PosDef

-

Boolean equality and comparisons

+

Boolean equality and comparisons

@@ -418,7 +418,7 @@

Library Corelib.BinNums.PosDef

-

A Square Root function for positive numbers

+

A Square Root function for positive numbers

@@ -566,7 +566,7 @@

Library Corelib.BinNums.PosDef

-

From binary positive numbers to Peano natural numbers

+

From binary positive numbers to Peano natural numbers

@@ -588,7 +588,7 @@

Library Corelib.BinNums.PosDef

-

From Peano natural numbers to binary positive numbers

+

From Peano natural numbers to binary positive numbers

diff --git a/v9.0/corelib/html/Corelib.Classes.CMorphisms.html b/v9.0/corelib/html/Corelib.Classes.CMorphisms.html index 641a9e35c4..cc2d3d2c27 100644 --- a/v9.0/corelib/html/Corelib.Classes.CMorphisms.html +++ b/v9.0/corelib/html/Corelib.Classes.CMorphisms.html @@ -49,7 +49,7 @@

Library Corelib.Classes.CMorphisms

-

Typeclass-based morphism definition and standard, minimal instances

+

Typeclass-based morphism definition and standard, minimal instances

@@ -78,7 +78,7 @@

Library Corelib.Classes.CMorphisms

-

Morphisms.

+

Morphisms.

diff --git a/v9.0/corelib/html/Corelib.Classes.CRelationClasses.html b/v9.0/corelib/html/Corelib.Classes.CRelationClasses.html index d95dae1877..c68009f1fb 100644 --- a/v9.0/corelib/html/Corelib.Classes.CRelationClasses.html +++ b/v9.0/corelib/html/Corelib.Classes.CRelationClasses.html @@ -49,7 +49,7 @@

Library Corelib.Classes.CRelationClasses

-

Typeclass-based relations, tactics and standard instances

+

Typeclass-based relations, tactics and standard instances

@@ -454,7 +454,7 @@

Library Corelib.Classes.CRelationClasses

We can already dualize all these properties.
-

Standard instances.

+

Standard instances.

@@ -607,7 +607,7 @@

Library Corelib.Classes.CRelationClasses

-

Partial Order.

+

Partial Order.

A partial order is a preorder which is additionally antisymmetric. We give an equivalent definition, up-to an equivalence crelation diff --git a/v9.0/corelib/html/Corelib.Classes.Equivalence.html b/v9.0/corelib/html/Corelib.Classes.Equivalence.html index ca41c2cff9..914d17c248 100644 --- a/v9.0/corelib/html/Corelib.Classes.Equivalence.html +++ b/v9.0/corelib/html/Corelib.Classes.Equivalence.html @@ -49,7 +49,7 @@

Library Corelib.Classes.Equivalence

-

Typeclass-based setoids. Definitions on Equivalence.

+

Typeclass-based setoids. Definitions on Equivalence.

diff --git a/v9.0/corelib/html/Corelib.Classes.Init.html b/v9.0/corelib/html/Corelib.Classes.Init.html index 19ff7d0edd..b934d830fe 100644 --- a/v9.0/corelib/html/Corelib.Classes.Init.html +++ b/v9.0/corelib/html/Corelib.Classes.Init.html @@ -49,7 +49,7 @@

Library Corelib.Classes.Init

-

Initialization code for typeclasses, setting up the default tactic

+

Initialization code for typeclasses, setting up the default tactic

for instance search. diff --git a/v9.0/corelib/html/Corelib.Classes.Morphisms.html b/v9.0/corelib/html/Corelib.Classes.Morphisms.html index e7d4171955..968215951b 100644 --- a/v9.0/corelib/html/Corelib.Classes.Morphisms.html +++ b/v9.0/corelib/html/Corelib.Classes.Morphisms.html @@ -49,7 +49,7 @@

Library Corelib.Classes.Morphisms

-

Typeclass-based morphism definition and standard, minimal instances

+

Typeclass-based morphism definition and standard, minimal instances

@@ -74,7 +74,7 @@

Library Corelib.Classes.Morphisms

-

Morphisms.

+

Morphisms.

diff --git a/v9.0/corelib/html/Corelib.Classes.Morphisms_Prop.html b/v9.0/corelib/html/Corelib.Classes.Morphisms_Prop.html index bec989bbbb..cf9cf6548b 100644 --- a/v9.0/corelib/html/Corelib.Classes.Morphisms_Prop.html +++ b/v9.0/corelib/html/Corelib.Classes.Morphisms_Prop.html @@ -49,7 +49,7 @@

Library Corelib.Classes.Morphisms_Prop

-

Proper instances for propositional connectives.

+

Proper instances for propositional connectives.

diff --git a/v9.0/corelib/html/Corelib.Classes.RelationClasses.html b/v9.0/corelib/html/Corelib.Classes.RelationClasses.html index c503d28b50..49531c8bd8 100644 --- a/v9.0/corelib/html/Corelib.Classes.RelationClasses.html +++ b/v9.0/corelib/html/Corelib.Classes.RelationClasses.html @@ -49,7 +49,7 @@

Library Corelib.Classes.RelationClasses

-

Typeclass-based relations, tactics and standard instances

+

Typeclass-based relations, tactics and standard instances

@@ -480,7 +480,7 @@

Library Corelib.Classes.RelationClasses

We can already dualize all these properties.
-

Standard instances.

+

Standard instances.

@@ -847,7 +847,7 @@

Library Corelib.Classes.RelationClasses

-

Partial Order.

+

Partial Order.

A partial order is a preorder which is additionally antisymmetric. We give an equivalent definition, up-to an equivalence relation diff --git a/v9.0/corelib/html/Corelib.Classes.SetoidTactics.html b/v9.0/corelib/html/Corelib.Classes.SetoidTactics.html index 99278f39bf..25f178b662 100644 --- a/v9.0/corelib/html/Corelib.Classes.SetoidTactics.html +++ b/v9.0/corelib/html/Corelib.Classes.SetoidTactics.html @@ -49,7 +49,7 @@

Library Corelib.Classes.SetoidTactics

-

Tactics for typeclass-based setoids.

+

Tactics for typeclass-based setoids.

diff --git a/v9.0/corelib/html/Corelib.Floats.FloatAxioms.html b/v9.0/corelib/html/Corelib.Floats.FloatAxioms.html index f8200651a0..aa30f78836 100644 --- a/v9.0/corelib/html/Corelib.Floats.FloatAxioms.html +++ b/v9.0/corelib/html/Corelib.Floats.FloatAxioms.html @@ -53,7 +53,7 @@

Library Corelib.Floats.FloatAxioms

-

Properties of the primitive operators for the Binary64 format

+

Properties of the primitive operators for the Binary64 format

diff --git a/v9.0/corelib/html/Corelib.Floats.FloatOps.html b/v9.0/corelib/html/Corelib.Floats.FloatOps.html index 28093d314b..5601caa876 100644 --- a/v9.0/corelib/html/Corelib.Floats.FloatOps.html +++ b/v9.0/corelib/html/Corelib.Floats.FloatOps.html @@ -53,7 +53,7 @@

Library Corelib.Floats.FloatOps

-

Derived operations and mapping between primitive floats and spec_floats

+

Derived operations and mapping between primitive floats and spec_floats

diff --git a/v9.0/corelib/html/Corelib.Floats.PrimFloat.html b/v9.0/corelib/html/Corelib.Floats.PrimFloat.html index 5af79794e4..447f857842 100644 --- a/v9.0/corelib/html/Corelib.Floats.PrimFloat.html +++ b/v9.0/corelib/html/Corelib.Floats.PrimFloat.html @@ -52,7 +52,7 @@

Library Corelib.Floats.PrimFloat

-

Definition of the interface for primitive floating-point arithmetic

+

Definition of the interface for primitive floating-point arithmetic

@@ -61,7 +61,7 @@

Library Corelib.Floats.PrimFloat

IEEE 754-2008 standard.
-

Type definition for the co-domain of compare

+

Type definition for the co-domain of compare

@@ -77,7 +77,7 @@

Library Corelib.Floats.PrimFloat

-

The main type

+

The main type

float: primitive type for Binary64 floating-point numbers.
@@ -95,7 +95,7 @@

Library Corelib.Floats.PrimFloat

-

Syntax support

+

Syntax support

@@ -110,7 +110,7 @@

Library Corelib.Floats.PrimFloat

-

Floating-point operators

+

Floating-point operators

@@ -185,7 +185,7 @@

Library Corelib.Floats.PrimFloat

-

Conversions

+

Conversions

@@ -224,7 +224,7 @@

Library Corelib.Floats.PrimFloat

-

Exponent manipulation functions

+

Exponent manipulation functions

frshiftexp: convert a float to fractional part in [0.5, 1.) and integer part.
@@ -244,7 +244,7 @@

Library Corelib.Floats.PrimFloat

-

Predecesor/Successor functions

+

Predecesor/Successor functions

@@ -266,7 +266,7 @@

Library Corelib.Floats.PrimFloat

-

Special values (needed for pretty-printing)

+

Special values (needed for pretty-printing)

@@ -283,7 +283,7 @@

Library Corelib.Floats.PrimFloat

-

Other special values

+

Other special values

@@ -296,7 +296,7 @@

Library Corelib.Floats.PrimFloat

-

Predicates and helper functions

+

Predicates and helper functions

diff --git a/v9.0/corelib/html/Corelib.Floats.SpecFloat.html b/v9.0/corelib/html/Corelib.Floats.SpecFloat.html index dcffa6d4a5..a2bdf25464 100644 --- a/v9.0/corelib/html/Corelib.Floats.SpecFloat.html +++ b/v9.0/corelib/html/Corelib.Floats.SpecFloat.html @@ -52,7 +52,7 @@

Library Corelib.Floats.SpecFloat

-

Specification of floating-point arithmetic

+

Specification of floating-point arithmetic

@@ -61,7 +61,7 @@

Library Corelib.Floats.SpecFloat

of the Flocq library (see http://flocq.gforge.inria.fr/)
-

Inductive specification of floating-point numbers

+

Inductive specification of floating-point numbers

@@ -79,7 +79,7 @@

Library Corelib.Floats.SpecFloat

-

Parameterized definitions

+

Parameterized definitions

@@ -242,7 +242,7 @@

Library Corelib.Floats.SpecFloat

-

Define operations

+

Define operations

diff --git a/v9.0/corelib/html/Corelib.Init.Byte.html b/v9.0/corelib/html/Corelib.Init.Byte.html index f57ba2b4f2..8578d35e77 100644 --- a/v9.0/corelib/html/Corelib.Init.Byte.html +++ b/v9.0/corelib/html/Corelib.Init.Byte.html @@ -49,7 +49,7 @@

Library Corelib.Init.Byte

-

Bytes

+

Bytes

diff --git a/v9.0/corelib/html/Corelib.Init.Datatypes.html b/v9.0/corelib/html/Corelib.Init.Datatypes.html index fd6a294849..46d15c4f4f 100644 --- a/v9.0/corelib/html/Corelib.Init.Datatypes.html +++ b/v9.0/corelib/html/Corelib.Init.Datatypes.html @@ -57,7 +57,7 @@

Library Corelib.Init.Datatypes

-

Datatypes with zero and one element

+

Datatypes with zero and one element

@@ -91,7 +91,7 @@

Library Corelib.Init.Datatypes

-

The boolean datatype

+

The boolean datatype

@@ -121,7 +121,7 @@

Library Corelib.Init.Datatypes

-

Reflect: a specialized inductive type for

+

Reflect: a specialized inductive type for

relating propositions and booleans, as popularized by the Ssreflect library. @@ -287,7 +287,7 @@

Library Corelib.Init.Datatypes

-

Peano natural numbers

+

Peano natural numbers

@@ -322,7 +322,7 @@

Library Corelib.Init.Datatypes

-

Container datatypes

+

Container datatypes

@@ -527,7 +527,7 @@

Library Corelib.Init.Datatypes

-

The comparison datatype

+

The comparison datatype

@@ -645,7 +645,7 @@

Library Corelib.Init.Datatypes

-

Misc Other Datatypes

+

Misc Other Datatypes

diff --git a/v9.0/corelib/html/Corelib.Init.Decimal.html b/v9.0/corelib/html/Corelib.Init.Decimal.html index 6c9083faef..ef895fa308 100644 --- a/v9.0/corelib/html/Corelib.Init.Decimal.html +++ b/v9.0/corelib/html/Corelib.Init.Decimal.html @@ -49,7 +49,7 @@

Library Corelib.Init.Decimal

-

Decimal numbers

+

Decimal numbers

diff --git a/v9.0/corelib/html/Corelib.Init.Hexadecimal.html b/v9.0/corelib/html/Corelib.Init.Hexadecimal.html index f151c727ea..2b017525c9 100644 --- a/v9.0/corelib/html/Corelib.Init.Hexadecimal.html +++ b/v9.0/corelib/html/Corelib.Init.Hexadecimal.html @@ -49,7 +49,7 @@

Library Corelib.Init.Hexadecimal

-

Hexadecimal numbers

+

Hexadecimal numbers

diff --git a/v9.0/corelib/html/Corelib.Init.Logic.html b/v9.0/corelib/html/Corelib.Init.Logic.html index 40bd4c6642..5543090c85 100644 --- a/v9.0/corelib/html/Corelib.Init.Logic.html +++ b/v9.0/corelib/html/Corelib.Init.Logic.html @@ -59,7 +59,7 @@

Library Corelib.Init.Logic

-

Propositional connectives

+

Propositional connectives

@@ -314,7 +314,7 @@

Library Corelib.Init.Logic

-

First-order quantifiers

+

First-order quantifiers

@@ -467,7 +467,7 @@

Library Corelib.Init.Logic

-

Equality

+

Equality

@@ -867,7 +867,7 @@

Library Corelib.Init.Logic

-

Being inhabited

+

Being inhabited

diff --git a/v9.0/corelib/html/Corelib.Init.Nat.html b/v9.0/corelib/html/Corelib.Init.Nat.html index 953d60cf11..57169025c2 100644 --- a/v9.0/corelib/html/Corelib.Init.Nat.html +++ b/v9.0/corelib/html/Corelib.Init.Nat.html @@ -54,7 +54,7 @@

Library Corelib.Init.Nat

-

Peano natural numbers, definitions of operations

+

Peano natural numbers, definitions of operations

@@ -71,7 +71,7 @@

Library Corelib.Init.Nat

-

Constants

+

Constants

@@ -90,7 +90,7 @@

Library Corelib.Init.Nat

-

Basic operations

+

Basic operations

@@ -159,7 +159,7 @@

Library Corelib.Init.Nat

-

Comparisons

+

Comparisons

@@ -205,7 +205,7 @@

Library Corelib.Init.Nat

-

Minimum, maximum

+

Minimum, maximum

@@ -230,7 +230,7 @@

Library Corelib.Init.Nat

-

Parity tests

+

Parity tests

@@ -250,7 +250,7 @@

Library Corelib.Init.Nat

-

Power

+

Power

@@ -268,7 +268,7 @@

Library Corelib.Init.Nat

-

Tail-recursive versions of add and mul

+

Tail-recursive versions of add and mul

@@ -302,7 +302,7 @@

Library Corelib.Init.Nat

-

Conversion with a decimal representation for printing/parsing

+

Conversion with a decimal representation for printing/parsing

@@ -426,7 +426,7 @@

Library Corelib.Init.Nat

-

Euclidean division

+

Euclidean division

@@ -469,7 +469,7 @@

Library Corelib.Init.Nat

-

Greatest common divisor

+

Greatest common divisor

@@ -491,7 +491,7 @@

Library Corelib.Init.Nat

-

Square

+

Square

@@ -503,7 +503,7 @@

Library Corelib.Init.Nat

-

Square root

+

Square root

@@ -541,7 +541,7 @@

Library Corelib.Init.Nat

-

Log2

+

Log2

diff --git a/v9.0/corelib/html/Corelib.Init.Number.html b/v9.0/corelib/html/Corelib.Init.Number.html index a50c5197b2..ac801ba181 100644 --- a/v9.0/corelib/html/Corelib.Init.Number.html +++ b/v9.0/corelib/html/Corelib.Init.Number.html @@ -49,7 +49,7 @@

Library Corelib.Init.Number

-

Decimal or Hexadecimal numbers

+

Decimal or Hexadecimal numbers

diff --git a/v9.0/corelib/html/Corelib.Init.Tactics.html b/v9.0/corelib/html/Corelib.Init.Tactics.html index 78d92fdca7..eb3302d86b 100644 --- a/v9.0/corelib/html/Corelib.Init.Tactics.html +++ b/v9.0/corelib/html/Corelib.Init.Tactics.html @@ -55,7 +55,7 @@

Library Corelib.Init.Tactics

-

Useful tactics

+

Useful tactics

@@ -376,7 +376,7 @@

Library Corelib.Init.Tactics

-

inversion_sigma

+

inversion_sigma

The built-in inversion will frequently leave equalities of dependent pairs. When the first type in the pair is an hProp or otherwise simplifies, inversion_sigma is useful; it will replace diff --git a/v9.0/corelib/html/Corelib.Init.Tauto.html b/v9.0/corelib/html/Corelib.Init.Tauto.html index 3d8d038cac..25ee4b6e04 100644 --- a/v9.0/corelib/html/Corelib.Init.Tauto.html +++ b/v9.0/corelib/html/Corelib.Init.Tauto.html @@ -49,7 +49,7 @@

Library Corelib.Init.Tauto

-

The tauto and intuition tactics

+

The tauto and intuition tactics

diff --git a/v9.0/corelib/html/Corelib.Init.Wf.html b/v9.0/corelib/html/Corelib.Init.Wf.html index a1b153e94f..c66cb62cf9 100644 --- a/v9.0/corelib/html/Corelib.Init.Wf.html +++ b/v9.0/corelib/html/Corelib.Init.Wf.html @@ -49,7 +49,7 @@

Library Corelib.Init.Wf

-

This module proves the validity of

+

This module proves the validity of

-

Basics: definition of polymorphic lists and some operations

+

Basics: definition of polymorphic lists and some operations

@@ -65,7 +65,7 @@

Library Corelib.Lists.ListDef

-

Map

+

Map

@@ -133,7 +133,7 @@

Library Corelib.Lists.ListDef

-

Nth element of a list

+

Nth element of a list

@@ -186,7 +186,7 @@

Library Corelib.Lists.ListDef

-

Existential and universal predicates over lists

+

Existential and universal predicates over lists

@@ -215,7 +215,7 @@

Library Corelib.Lists.ListDef

-

List comparison

+

List comparison

diff --git a/v9.0/corelib/html/Corelib.Strings.PrimStringAxioms.html b/v9.0/corelib/html/Corelib.Strings.PrimStringAxioms.html index 755973e695..7ecc232a4d 100644 --- a/v9.0/corelib/html/Corelib.Strings.PrimStringAxioms.html +++ b/v9.0/corelib/html/Corelib.Strings.PrimStringAxioms.html @@ -56,7 +56,7 @@

Library Corelib.Strings.PrimStringAxioms

-

Conversion to / from lists

+

Conversion to / from lists

@@ -95,7 +95,7 @@

Library Corelib.Strings.PrimStringAxioms

-

Axioms relating string operations with list operations

+

Axioms relating string operations with list operations

diff --git a/v9.0/corelib/html/index_global_T.html b/v9.0/corelib/html/index_global_T.html index 40fb9de90c..580bde376b 100644 --- a/v9.0/corelib/html/index_global_T.html +++ b/v9.0/corelib/html/index_global_T.html @@ -525,8 +525,8 @@

T

t [definition, in Corelib.Init.Nat]
-Tactics [library]
Tactics [library]
+Tactics [library]
tactic_view [constructor, in Corelib.ssr.ssreflect]
tag [definition, in Corelib.ssr.ssrfun]
Tag [section, in Corelib.ssr.ssrfun]
diff --git a/v9.0/corelib/html/index_global_W.html b/v9.0/corelib/html/index_global_W.html index 2fd5dad502..a1904ed42c 100644 --- a/v9.0/corelib/html/index_global_W.html +++ b/v9.0/corelib/html/index_global_W.html @@ -554,8 +554,8 @@ Well_founded.R [variable, in Corelib.Init.Wf]
Well_founded.A [variable, in Corelib.Init.Wf]
Well_founded [section, in Corelib.Init.Wf]
-Wf [library]
Wf [library]
+Wf [library]
wlog_neg [lemma, in Corelib.ssr.ssrbool]
wrap [definition, in Corelib.ssr.ssrfun]
wrapped [record, in Corelib.ssr.ssrfun]
diff --git a/v9.0/corelib/html/index_library_T.html b/v9.0/corelib/html/index_library_T.html index 53c5406f6f..8a60059762 100644 --- a/v9.0/corelib/html/index_library_T.html +++ b/v9.0/corelib/html/index_library_T.html @@ -524,8 +524,8 @@

T (library)

-Tactics
Tactics
+Tactics
Tauto
TransparentState


diff --git a/v9.0/corelib/html/index_library_W.html b/v9.0/corelib/html/index_library_W.html index cf6f12a978..a2ae58cede 100644 --- a/v9.0/corelib/html/index_library_W.html +++ b/v9.0/corelib/html/index_library_W.html @@ -524,8 +524,8 @@

W (library)

-Wf
Wf
+Wf


-

Reflect: a specialized inductive type for

+

Reflect: a specialized inductive type for

relating propositions and booleans, as popularized by the Ssreflect library. diff --git a/v9.0/stdlib/Stdlib.Bool.BoolOrder.html b/v9.0/stdlib/Stdlib.Bool.BoolOrder.html index a9bc31c3e8..79afaabcd5 100644 --- a/v9.0/stdlib/Stdlib.Bool.BoolOrder.html +++ b/v9.0/stdlib/Stdlib.Bool.BoolOrder.html @@ -65,7 +65,7 @@

Library Stdlib.Bool.BoolOrder

-

Order le

+

Order le

@@ -91,7 +91,7 @@

Library Stdlib.Bool.BoolOrder

-

Strict order lt

+

Strict order lt

@@ -126,7 +126,7 @@

Library Stdlib.Bool.BoolOrder

-

Order structures

+

Order structures

diff --git a/v9.0/stdlib/Stdlib.Classes.CEquivalence.html b/v9.0/stdlib/Stdlib.Classes.CEquivalence.html index d327cbf2cb..90ea3c5ea8 100644 --- a/v9.0/stdlib/Stdlib.Classes.CEquivalence.html +++ b/v9.0/stdlib/Stdlib.Classes.CEquivalence.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.CEquivalence

-

Typeclass-based setoids. Definitions on Equivalence.

+

Typeclass-based setoids. Definitions on Equivalence.

diff --git a/v9.0/stdlib/Stdlib.Classes.DecidableClass.html b/v9.0/stdlib/Stdlib.Classes.DecidableClass.html index 0800f7bcf5..621e93396f 100644 --- a/v9.0/stdlib/Stdlib.Classes.DecidableClass.html +++ b/v9.0/stdlib/Stdlib.Classes.DecidableClass.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.DecidableClass

-

A typeclass to ease the handling of decidable properties.

+

A typeclass to ease the handling of decidable properties.

diff --git a/v9.0/stdlib/Stdlib.Classes.EquivDec.html b/v9.0/stdlib/Stdlib.Classes.EquivDec.html index 1cf59bb78a..de0eb7d770 100644 --- a/v9.0/stdlib/Stdlib.Classes.EquivDec.html +++ b/v9.0/stdlib/Stdlib.Classes.EquivDec.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.EquivDec

-

Decidable equivalences.

+

Decidable equivalences.

diff --git a/v9.0/stdlib/Stdlib.Classes.Morphisms_Relations.html b/v9.0/stdlib/Stdlib.Classes.Morphisms_Relations.html index a52426afb8..44162e9650 100644 --- a/v9.0/stdlib/Stdlib.Classes.Morphisms_Relations.html +++ b/v9.0/stdlib/Stdlib.Classes.Morphisms_Relations.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.Morphisms_Relations

-

Morphism instances for relations.

+

Morphism instances for relations.

diff --git a/v9.0/stdlib/Stdlib.Classes.RelationPairs.html b/v9.0/stdlib/Stdlib.Classes.RelationPairs.html index a59c22d3ce..caba9bf724 100644 --- a/v9.0/stdlib/Stdlib.Classes.RelationPairs.html +++ b/v9.0/stdlib/Stdlib.Classes.RelationPairs.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.RelationPairs

-

Relations over pairs

+

Relations over pairs

diff --git a/v9.0/stdlib/Stdlib.Classes.SetoidClass.html b/v9.0/stdlib/Stdlib.Classes.SetoidClass.html index c143f05d63..40e6df6f9c 100644 --- a/v9.0/stdlib/Stdlib.Classes.SetoidClass.html +++ b/v9.0/stdlib/Stdlib.Classes.SetoidClass.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.SetoidClass

-

Typeclass-based setoids, tactics and standard instances.

+

Typeclass-based setoids, tactics and standard instances.

diff --git a/v9.0/stdlib/Stdlib.Classes.SetoidDec.html b/v9.0/stdlib/Stdlib.Classes.SetoidDec.html index 7daab39ab6..0f1d38fbe7 100644 --- a/v9.0/stdlib/Stdlib.Classes.SetoidDec.html +++ b/v9.0/stdlib/Stdlib.Classes.SetoidDec.html @@ -48,7 +48,7 @@

Library Stdlib.Classes.SetoidDec

-

Decidable setoid equality theory.

+

Decidable setoid equality theory.

diff --git a/v9.0/stdlib/Stdlib.FSets.FMapAVL.html b/v9.0/stdlib/Stdlib.FSets.FMapAVL.html index 72def82159..0daccf7df5 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapAVL.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapAVL.html @@ -50,7 +50,7 @@

Library Stdlib.FSets.FMapAVL

-

FMapAVL

+

FMapAVL

@@ -87,7 +87,7 @@

Library Stdlib.FSets.FMapAVL

-

The Raw functor

+

The Raw functor

@@ -113,11 +113,11 @@

Library Stdlib.FSets.FMapAVL

-

Trees

+

Trees

-

Trees

+

Trees

@@ -149,7 +149,7 @@

Library Stdlib.FSets.FMapAVL

-

Basic functions on trees: height and cardinal

+

Basic functions on trees: height and cardinal

@@ -172,7 +172,7 @@

Library Stdlib.FSets.FMapAVL

-

Empty Map

+

Empty Map

@@ -184,7 +184,7 @@

Library Stdlib.FSets.FMapAVL

-

Emptyness test

+

Emptyness test

@@ -196,7 +196,7 @@

Library Stdlib.FSets.FMapAVL

-

Membership

+

Membership

@@ -231,7 +231,7 @@

Library Stdlib.FSets.FMapAVL

-

Helper functions

+

Helper functions

@@ -294,7 +294,7 @@

Library Stdlib.FSets.FMapAVL

-

Insertion

+

Insertion

@@ -315,7 +315,7 @@

Library Stdlib.FSets.FMapAVL

-

Extraction of minimum binding

+

Extraction of minimum binding

@@ -340,7 +340,7 @@

Library Stdlib.FSets.FMapAVL

-

Merging two trees

+

Merging two trees

@@ -366,7 +366,7 @@

Library Stdlib.FSets.FMapAVL

-

Deletion

+

Deletion

@@ -386,7 +386,7 @@

Library Stdlib.FSets.FMapAVL

-

join

+

join

@@ -415,7 +415,7 @@

Library Stdlib.FSets.FMapAVL

-

Splitting

+

Splitting

@@ -455,7 +455,7 @@

Library Stdlib.FSets.FMapAVL

-

Concatenation

+

Concatenation

@@ -479,7 +479,7 @@

Library Stdlib.FSets.FMapAVL

-

Elements

+

Elements

@@ -510,7 +510,7 @@

Library Stdlib.FSets.FMapAVL

-

Fold

+

Fold

@@ -526,7 +526,7 @@

Library Stdlib.FSets.FMapAVL

-

Comparison

+

Comparison

@@ -538,7 +538,7 @@

Library Stdlib.FSets.FMapAVL

-

Enumeration of the elements of a tree

+

Enumeration of the elements of a tree

@@ -637,7 +637,7 @@

Library Stdlib.FSets.FMapAVL

-

Map

+

Map

@@ -662,7 +662,7 @@

Library Stdlib.FSets.FMapAVL

-

Map with removal

+

Map with removal

@@ -683,7 +683,7 @@

Library Stdlib.FSets.FMapAVL

-

Optimized map2

+

Optimized map2

@@ -739,7 +739,7 @@

Library Stdlib.FSets.FMapAVL

-

Map2

+

Map2

@@ -769,7 +769,7 @@

Library Stdlib.FSets.FMapAVL

-

Invariants

+

Invariants

@@ -782,7 +782,7 @@

Library Stdlib.FSets.FMapAVL

-

Occurrence in a tree

+

Occurrence in a tree

@@ -812,7 +812,7 @@

Library Stdlib.FSets.FMapAVL

-

Binary search trees

+

Binary search trees

@@ -846,7 +846,7 @@

Library Stdlib.FSets.FMapAVL

-

Correctness proofs, isolated in a sub-module

+

Correctness proofs, isolated in a sub-module

@@ -1138,7 +1138,7 @@

Library Stdlib.FSets.FMapAVL

-

Automation and dedicated tactics.

+

Automation and dedicated tactics.

@@ -1249,7 +1249,7 @@

Library Stdlib.FSets.FMapAVL

-

Basic results about MapsTo, In, lt_tree, gt_tree, height

+

Basic results about MapsTo, In, lt_tree, gt_tree, height

@@ -1353,7 +1353,7 @@

Library Stdlib.FSets.FMapAVL

-

Empty map

+

Empty map

@@ -1371,7 +1371,7 @@

Library Stdlib.FSets.FMapAVL

-

Emptyness test

+

Emptyness test

@@ -1386,7 +1386,7 @@

Library Stdlib.FSets.FMapAVL

-

Membership

+

Membership

@@ -1440,7 +1440,7 @@

Library Stdlib.FSets.FMapAVL

-

Helper functions

+

Helper functions

@@ -1480,7 +1480,7 @@

Library Stdlib.FSets.FMapAVL

-

Insertion

+

Insertion

@@ -1514,7 +1514,7 @@

Library Stdlib.FSets.FMapAVL

-

Extraction of minimum binding

+

Extraction of minimum binding

@@ -1557,7 +1557,7 @@

Library Stdlib.FSets.FMapAVL

-

Merging two trees

+

Merging two trees

@@ -1579,7 +1579,7 @@

Library Stdlib.FSets.FMapAVL

-

Deletion

+

Deletion

@@ -1606,7 +1606,7 @@

Library Stdlib.FSets.FMapAVL

-

join

+

join

@@ -1630,7 +1630,7 @@

Library Stdlib.FSets.FMapAVL

-

split

+

split

@@ -1669,7 +1669,7 @@

Library Stdlib.FSets.FMapAVL

-

Concatenation

+

Concatenation

@@ -1695,7 +1695,7 @@

Library Stdlib.FSets.FMapAVL

-

Elements

+

Elements

@@ -1749,7 +1749,7 @@

Library Stdlib.FSets.FMapAVL

-

Fold

+

Fold

@@ -1777,7 +1777,7 @@

Library Stdlib.FSets.FMapAVL

-

Comparison

+

Comparison

@@ -2004,7 +2004,7 @@

Library Stdlib.FSets.FMapAVL

-

Encapsulation

+

Encapsulation

diff --git a/v9.0/stdlib/Stdlib.FSets.FMapFacts.html b/v9.0/stdlib/Stdlib.FSets.FMapFacts.html index 7a7808a452..c9b56b4b0f 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapFacts.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapFacts.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FMapFacts

-

Finite maps library

+

Finite maps library

@@ -75,7 +75,7 @@

Library Stdlib.FSets.FMapFacts

-

Facts about weak maps

+

Facts about weak maps

@@ -102,7 +102,7 @@

Library Stdlib.FSets.FMapFacts

-

Specifications written using equivalences

+

Specifications written using equivalences

@@ -259,7 +259,7 @@

Library Stdlib.FSets.FMapFacts

-

Specifications written using boolean predicates

+

Specifications written using boolean predicates

@@ -398,7 +398,7 @@

Library Stdlib.FSets.FMapFacts

-

Relations between Equal, Equiv and Equivb.

+

Relations between Equal, Equiv and Equivb.

@@ -460,7 +460,7 @@

Library Stdlib.FSets.FMapFacts

-

Equal is a setoid equality.

+

Equal is a setoid equality.

@@ -544,7 +544,7 @@

Library Stdlib.FSets.FMapFacts

-

Same facts for self-contained weak sets and for full maps

+

Same facts for self-contained weak sets and for full maps

@@ -557,7 +557,7 @@

Library Stdlib.FSets.FMapFacts

-

Additional Properties for weak maps

+

Additional Properties for weak maps

@@ -617,7 +617,7 @@

Library Stdlib.FSets.FMapFacts

-

Elements

+

Elements

@@ -632,7 +632,7 @@

Library Stdlib.FSets.FMapFacts

-

Conversions between maps and association lists.

+

Conversions between maps and association lists.

@@ -669,7 +669,7 @@

Library Stdlib.FSets.FMapFacts

-

Fold

+

Fold

@@ -685,7 +685,7 @@

Library Stdlib.FSets.FMapFacts

-

Induction principles about fold contributed by S. Lescuyer

+

Induction principles about fold contributed by S. Lescuyer

@@ -798,7 +798,7 @@

Library Stdlib.FSets.FMapFacts

-

Additional properties of fold

+

Additional properties of fold

@@ -893,7 +893,7 @@

Library Stdlib.FSets.FMapFacts

-

Cardinal

+

Cardinal

@@ -939,7 +939,7 @@

Library Stdlib.FSets.FMapFacts

-

Additional notions over maps

+

Additional notions over maps

@@ -957,7 +957,7 @@

Library Stdlib.FSets.FMapFacts

-

Emulation of some functions lacking in the interface

+

Emulation of some functions lacking in the interface

@@ -1184,7 +1184,7 @@

Library Stdlib.FSets.FMapFacts

-

Same Properties for self-contained weak maps and for full maps

+

Same Properties for self-contained weak maps and for full maps

@@ -1197,7 +1197,7 @@

Library Stdlib.FSets.FMapFacts

-

Properties specific to maps with ordered keys

+

Properties specific to maps with ordered keys

diff --git a/v9.0/stdlib/Stdlib.FSets.FMapFullAVL.html b/v9.0/stdlib/Stdlib.FSets.FMapFullAVL.html index 0d8e79e500..c1d1f02529 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapFullAVL.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapFullAVL.html @@ -50,7 +50,7 @@

Library Stdlib.FSets.FMapFullAVL

-

FMapFullAVL

+

FMapFullAVL

@@ -119,7 +119,7 @@

Library Stdlib.FSets.FMapFullAVL

-

AVL trees

+

AVL trees

@@ -143,7 +143,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Automation and dedicated tactics about avl.

+

Automation and dedicated tactics about avl.

@@ -181,7 +181,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Basic results about avl, height

+

Basic results about avl, height

@@ -209,7 +209,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Empty map

+

Empty map

@@ -221,7 +221,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Helper functions

+

Helper functions

@@ -261,7 +261,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Insertion

+

Insertion

@@ -279,7 +279,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Extraction of minimum binding

+

Extraction of minimum binding

@@ -297,7 +297,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Merging two trees

+

Merging two trees

@@ -316,7 +316,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Deletion

+

Deletion

@@ -334,7 +334,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Join

+

Join

@@ -453,7 +453,7 @@

Library Stdlib.FSets.FMapFullAVL

-

Encapsulation

+

Encapsulation

@@ -652,7 +652,7 @@

Library Stdlib.FSets.FMapFullAVL

-

As comparison function, we propose here a non-structural

+

As comparison function, we propose here a non-structural

version faithful to the code of Ocaml's Map library, instead of the structural version of FMapAVL diff --git a/v9.0/stdlib/Stdlib.FSets.FMapInterface.html b/v9.0/stdlib/Stdlib.FSets.FMapInterface.html index 9ec6b5f4a1..f5d48af4ba 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapInterface.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapInterface.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FMapInterface

-

Finite map library

+

Finite map library

@@ -134,7 +134,7 @@

Library Stdlib.FSets.FMapInterface

-

Weak signature for maps

+

Weak signature for maps

@@ -555,7 +555,7 @@

Library Stdlib.FSets.FMapInterface

-

Static signature for Weak Maps

+

Static signature for Weak Maps

@@ -574,7 +574,7 @@

Library Stdlib.FSets.FMapInterface

-

Maps on ordered keys, functorial signature

+

Maps on ordered keys, functorial signature

@@ -601,7 +601,7 @@

Library Stdlib.FSets.FMapInterface

-

Maps on ordered keys, self-contained signature

+

Maps on ordered keys, self-contained signature

@@ -616,7 +616,7 @@

Library Stdlib.FSets.FMapInterface

-

Maps with ordering both on keys and datas

+

Maps with ordering both on keys and datas

diff --git a/v9.0/stdlib/Stdlib.FSets.FMapList.html b/v9.0/stdlib/Stdlib.FSets.FMapList.html index 618ed691a9..c3874e7b36 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapList.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapList.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FMapList

-

Finite map library

+

Finite map library

@@ -92,7 +92,7 @@

Library Stdlib.FSets.FMapList

-

empty

+

empty

@@ -115,7 +115,7 @@

Library Stdlib.FSets.FMapList

-

is_empty

+

is_empty

@@ -133,7 +133,7 @@

Library Stdlib.FSets.FMapList

-

mem

+

mem

@@ -160,7 +160,7 @@

Library Stdlib.FSets.FMapList

-

find

+

find

@@ -187,7 +187,7 @@

Library Stdlib.FSets.FMapList

-

add

+

add

@@ -228,7 +228,7 @@

Library Stdlib.FSets.FMapList

-

remove

+

remove

@@ -269,7 +269,7 @@

Library Stdlib.FSets.FMapList

-

elements

+

elements

@@ -295,7 +295,7 @@

Library Stdlib.FSets.FMapList

-

fold

+

fold

@@ -315,7 +315,7 @@

Library Stdlib.FSets.FMapList

-

equal

+

equal

@@ -365,7 +365,7 @@

Library Stdlib.FSets.FMapList

-

map and mapi

+

map and mapi

@@ -458,7 +458,7 @@

Library Stdlib.FSets.FMapList

-

map2

+

map2

diff --git a/v9.0/stdlib/Stdlib.FSets.FMapPositive.html b/v9.0/stdlib/Stdlib.FSets.FMapPositive.html index a8c45fc424..8b3443089d 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapPositive.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapPositive.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FMapPositive

-

FMapPositive : an implementation of FMapInterface for positive keys.

+

FMapPositive : an implementation of FMapInterface for positive keys.

diff --git a/v9.0/stdlib/Stdlib.FSets.FMapWeakList.html b/v9.0/stdlib/Stdlib.FSets.FMapWeakList.html index 998f7abea5..93cbb9c45e 100644 --- a/v9.0/stdlib/Stdlib.FSets.FMapWeakList.html +++ b/v9.0/stdlib/Stdlib.FSets.FMapWeakList.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FMapWeakList

-

Finite map library

+

Finite map library

@@ -90,7 +90,7 @@

Library Stdlib.FSets.FMapWeakList

-

empty

+

empty

@@ -115,7 +115,7 @@

Library Stdlib.FSets.FMapWeakList

-

is_empty

+

is_empty

@@ -133,7 +133,7 @@

Library Stdlib.FSets.FMapWeakList

-

mem

+

mem

@@ -155,7 +155,7 @@

Library Stdlib.FSets.FMapWeakList

-

find

+

find

@@ -184,7 +184,7 @@

Library Stdlib.FSets.FMapWeakList

-

add

+

add

@@ -228,7 +228,7 @@

Library Stdlib.FSets.FMapWeakList

-

remove

+

remove

@@ -262,7 +262,7 @@

Library Stdlib.FSets.FMapWeakList

-

elements

+

elements

@@ -283,7 +283,7 @@

Library Stdlib.FSets.FMapWeakList

-

fold

+

fold

@@ -303,7 +303,7 @@

Library Stdlib.FSets.FMapWeakList

-

equal

+

equal

@@ -364,7 +364,7 @@

Library Stdlib.FSets.FMapWeakList

-

map and mapi

+

map and mapi

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetAVL.html b/v9.0/stdlib/Stdlib.FSets.FSetAVL.html index e2ae94f933..759b6336fd 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetAVL.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetAVL.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetAVL

-

FSetAVL : Implementation of FSetInterface via AVL trees

+

FSetAVL : Implementation of FSetInterface via AVL trees

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetBridge.html b/v9.0/stdlib/Stdlib.FSets.FSetBridge.html index c91598d2db..2b36a95abf 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetBridge.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetBridge.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetBridge

-

Finite sets library

+

Finite sets library

@@ -65,7 +65,7 @@

Library Stdlib.FSets.FSetBridge

-

From non-dependent signature S to dependent signature Sdep.

+

From non-dependent signature S to dependent signature Sdep.

@@ -243,7 +243,7 @@

Library Stdlib.FSets.FSetBridge

-

From dependent signature Sdep to non-dependent signature S.

+

From dependent signature Sdep to non-dependent signature S.

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetCompat.html b/v9.0/stdlib/Stdlib.FSets.FSetCompat.html index e8487619a8..e3f9c1002b 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetCompat.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetCompat.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetCompat

-

Compatibility functors between FSetInterface and MSetInterface.

+

Compatibility functors between FSetInterface and MSetInterface.

@@ -64,7 +64,7 @@

Library Stdlib.FSets.FSetCompat

-

From new Weak Sets to old ones

+

From new Weak Sets to old ones

@@ -227,7 +227,7 @@

Library Stdlib.FSets.FSetCompat

-

From new Sets to new ones

+

From new Sets to new ones

@@ -285,7 +285,7 @@

Library Stdlib.FSets.FSetCompat

-

From old Weak Sets to new ones.

+

From old Weak Sets to new ones.

@@ -428,7 +428,7 @@

Library Stdlib.FSets.FSetCompat

-

From old Sets to new ones.

+

From old Sets to new ones.

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetDecide.html b/v9.0/stdlib/Stdlib.FSets.FSetDecide.html index 1e3d184497..305b808f70 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetDecide.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetDecide.html @@ -74,7 +74,7 @@

Library Stdlib.FSets.FSetDecide

-

Overview

+

Overview

This functor defines the tactic fsetdec, which will solve any valid goal of the form @@ -180,7 +180,7 @@

Library Stdlib.FSets.FSetDecide

-

Facts and Tactics for Propositional Logic

+

Facts and Tactics for Propositional Logic

These lemmas and tactics are in a module so that they do not affect the namespace if you import the enclosing @@ -195,18 +195,18 @@

Library Stdlib.FSets.FSetDecide

-

Lemmas and Tactics About Decidable Propositions

+

Lemmas and Tactics About Decidable Propositions

-

Propositional Equivalences Involving Negation

+

Propositional Equivalences Involving Negation

These are all written with the unfolded form of negation, since I am not sure if setoid rewriting will always perform conversion.
-

Tactics for Negations

+

Tactics for Negations

@@ -457,7 +457,7 @@

Library Stdlib.FSets.FSetDecide

-

Auxiliary Tactics

+

Auxiliary Tactics

Again, these lemmas and tactics are in a module so that they do not affect the namespace if you import the @@ -470,7 +470,7 @@

Library Stdlib.FSets.FSetDecide

-

Generic Tactics

+

Generic Tactics

We begin by defining a few generic, useful tactics.
@@ -587,7 +587,7 @@

Library Stdlib.FSets.FSetDecide

-

Discarding Irrelevant Hypotheses

+

Discarding Irrelevant Hypotheses

We will want to clear the context of any non-FSet-related hypotheses in order to increase the @@ -667,7 +667,7 @@

Library Stdlib.FSets.FSetDecide

-

Turning Set Operators into Propositional Connectives

+

Turning Set Operators into Propositional Connectives

The lemmas from FSetFacts will be used to break down set operations into propositional formulas built over @@ -693,7 +693,7 @@

Library Stdlib.FSets.FSetDecide

-

Decidability of FSet Propositions

+

Decidability of FSet Propositions

@@ -728,7 +728,7 @@

Library Stdlib.FSets.FSetDecide

-

Normalizing Propositions About Equality

+

Normalizing Propositions About Equality

We have to deal with the fact that E.eq may be convertible with Coq's equality. Thus, we will find the @@ -811,7 +811,7 @@

Library Stdlib.FSets.FSetDecide

-

Considering Decidability of Base Propositions

+

Considering Decidability of Base Propositions

This tactic adds assertions about the decidability of E.eq and In to the context. This is necessary for @@ -860,7 +860,7 @@

Library Stdlib.FSets.FSetDecide

-

Handling Empty, Subset, and Equal

+

Handling Empty, Subset, and Equal

This tactic instantiates universally quantified hypotheses (which arise from the unfolding of Empty, @@ -908,7 +908,7 @@

Library Stdlib.FSets.FSetDecide

-

The Core fsetdec Auxiliary Tactics

+

The Core fsetdec Auxiliary Tactics

@@ -950,7 +950,7 @@

Library Stdlib.FSets.FSetDecide

-

The fsetdec Tactic

+

The fsetdec Tactic

Here is the top-level tactic (the only one intended for clients of this library). It's specification is given at @@ -1064,7 +1064,7 @@

Library Stdlib.FSets.FSetDecide

-

Examples

+

Examples

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetEqProperties.html b/v9.0/stdlib/Stdlib.FSets.FSetEqProperties.html index bff665e7e1..08d5a59c1e 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetEqProperties.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetEqProperties.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetEqProperties

-

Finite sets library

+

Finite sets library

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetInterface.html b/v9.0/stdlib/Stdlib.FSets.FSetInterface.html index f7459e5256..f28b845a05 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetInterface.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetInterface.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetInterface

-

Finite set library

+

Finite set library

@@ -104,7 +104,7 @@

Library Stdlib.FSets.FSetInterface

-

Non-dependent signatures

+

Non-dependent signatures

@@ -113,7 +113,7 @@

Library Stdlib.FSets.FSetInterface

programs together with axioms
-

Functorial signature for weak sets

+

Functorial signature for weak sets

@@ -618,7 +618,7 @@

Library Stdlib.FSets.FSetInterface

-

Static signature for weak sets

+

Static signature for weak sets

@@ -638,7 +638,7 @@

Library Stdlib.FSets.FSetInterface

-

Functorial signature for sets on ordered elements

+

Functorial signature for sets on ordered elements

@@ -765,7 +765,7 @@

Library Stdlib.FSets.FSetInterface

-

Static signature for sets on ordered elements

+

Static signature for sets on ordered elements

@@ -785,7 +785,7 @@

Library Stdlib.FSets.FSetInterface

-

Some subtyping tests

+

Some subtyping tests

 WSfun ---> WS
@@ -802,7 +802,7 @@ 
Library Stdlib.FSets.FSetInterface

 
 
 

 
-
Dependent signature

+
Dependent signature

 
 
 
 

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetList.html b/v9.0/stdlib/Stdlib.FSets.FSetList.html
index fba26c95fd..1ed974abb6 100644
--- a/v9.0/stdlib/Stdlib.FSets.FSetList.html
+++ b/v9.0/stdlib/Stdlib.FSets.FSetList.html
@@ -48,7 +48,7 @@ 
Library Stdlib.FSets.FSetList
-

Finite sets library

+

Finite sets library

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetProperties.html b/v9.0/stdlib/Stdlib.FSets.FSetProperties.html index bdbe51be44..e47e3e1cb4 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetProperties.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetProperties.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetProperties

-

Finite sets library

+

Finite sets library

@@ -340,7 +340,7 @@

Library Stdlib.FSets.FSetProperties

-

Properties of elements

+

Properties of elements

@@ -355,7 +355,7 @@

Library Stdlib.FSets.FSetProperties

-

Conversions between lists and sets

+

Conversions between lists and sets

@@ -379,7 +379,7 @@

Library Stdlib.FSets.FSetProperties

-

Fold

+

Fold

@@ -407,7 +407,7 @@

Library Stdlib.FSets.FSetProperties

-

Induction principles for fold (contributed by S. Lescuyer)

+

Induction principles for fold (contributed by S. Lescuyer)

@@ -513,7 +513,7 @@

Library Stdlib.FSets.FSetProperties

-

Alternative (weaker) specifications for fold

+

Alternative (weaker) specifications for fold

@@ -585,7 +585,7 @@

Library Stdlib.FSets.FSetProperties

-

Fold is a morphism

+

Fold is a morphism

@@ -602,7 +602,7 @@

Library Stdlib.FSets.FSetProperties

-

Fold and other set operators

+

Fold and other set operators

@@ -654,11 +654,11 @@

Library Stdlib.FSets.FSetProperties

-

Cardinal

+

Cardinal

-

Characterization of cardinal in terms of fold

+

Characterization of cardinal in terms of fold

@@ -670,7 +670,7 @@

Library Stdlib.FSets.FSetProperties

-

Old specifications for cardinal.

+

Old specifications for cardinal.

@@ -693,7 +693,7 @@

Library Stdlib.FSets.FSetProperties

-

Cardinal and (non-)emptiness

+

Cardinal and (non-)emptiness

@@ -718,7 +718,7 @@

Library Stdlib.FSets.FSetProperties

-

Cardinal is a morphism

+

Cardinal is a morphism

@@ -737,7 +737,7 @@

Library Stdlib.FSets.FSetProperties

-

Cardinal and set operators

+

Cardinal and set operators

diff --git a/v9.0/stdlib/Stdlib.FSets.FSetToFiniteSet.html b/v9.0/stdlib/Stdlib.FSets.FSetToFiniteSet.html index 3a5be933bd..d167ef05b1 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetToFiniteSet.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetToFiniteSet.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetToFiniteSet

-

Finite sets library : conversion to old Finite_sets

+

Finite sets library : conversion to old Finite_sets

@@ -61,7 +61,7 @@

Library Stdlib.FSets.FSetToFiniteSet

-

Going from FSets with usual Leibniz equality

+

Going from FSets with usual Leibniz equality

to the good old Ensembles and Finite_sets theory.
diff --git a/v9.0/stdlib/Stdlib.FSets.FSetWeakList.html b/v9.0/stdlib/Stdlib.FSets.FSetWeakList.html index a960554790..304982c970 100644 --- a/v9.0/stdlib/Stdlib.FSets.FSetWeakList.html +++ b/v9.0/stdlib/Stdlib.FSets.FSetWeakList.html @@ -48,7 +48,7 @@

Library Stdlib.FSets.FSetWeakList

-

Finite sets library

+

Finite sets library

diff --git a/v9.0/stdlib/Stdlib.Floats.FloatLemmas.html b/v9.0/stdlib/Stdlib.Floats.FloatLemmas.html index 8deaec344a..796cfa7cc5 100644 --- a/v9.0/stdlib/Stdlib.Floats.FloatLemmas.html +++ b/v9.0/stdlib/Stdlib.Floats.FloatLemmas.html @@ -52,7 +52,7 @@

Library Stdlib.Floats.FloatLemmas

-

Support results involving frexp and ldexp

+

Support results involving frexp and ldexp

diff --git a/v9.0/stdlib/Stdlib.Lists.List.html b/v9.0/stdlib/Stdlib.Lists.List.html index 837669a5ec..e0fdfb87fc 100644 --- a/v9.0/stdlib/Stdlib.Lists.List.html +++ b/v9.0/stdlib/Stdlib.Lists.List.html @@ -56,7 +56,7 @@

Library Stdlib.Lists.List

-

Basics: definition of polymorphic lists and some operations

+

Basics: definition of polymorphic lists and some operations

@@ -148,7 +148,7 @@

Library Stdlib.Lists.List

-

Generic facts

+

Generic facts

@@ -183,7 +183,7 @@

Library Stdlib.Lists.List

-

Head and tail

+

Head and tail

@@ -198,7 +198,7 @@

Library Stdlib.Lists.List

-

Facts about app

+

Facts about app

@@ -319,7 +319,7 @@

Library Stdlib.Lists.List

-

Facts about In

+

Facts about In

@@ -406,7 +406,7 @@

Library Stdlib.Lists.List

-

Operations on the elements of a list

+

Operations on the elements of a list

@@ -421,7 +421,7 @@

Library Stdlib.Lists.List

-

Nth element of a list

+

Nth element of a list

@@ -617,7 +617,7 @@

Library Stdlib.Lists.List

-

Last element of a list

+

Last element of a list

@@ -672,7 +672,7 @@

Library Stdlib.Lists.List

-

Remove

+

Remove

@@ -723,7 +723,7 @@

Library Stdlib.Lists.List

-

Counting occurrences of an element

+

Counting occurrences of an element

@@ -787,7 +787,7 @@

Library Stdlib.Lists.List

-

Manipulating whole lists

+

Manipulating whole lists

@@ -802,7 +802,7 @@

Library Stdlib.Lists.List

-

Reverse

+

Reverse

@@ -899,7 +899,7 @@

Library Stdlib.Lists.List

-

Concatenation

+

Concatenation

@@ -928,7 +928,7 @@

Library Stdlib.Lists.List

-

Decidable equality on lists

+

Decidable equality on lists

@@ -949,11 +949,11 @@

Library Stdlib.Lists.List

-

Applying functions to the elements of a list

+

Applying functions to the elements of a list

-

Map

+

Map

@@ -1041,7 +1041,7 @@

Library Stdlib.Lists.List

-

Flat Map

+

Flat Map

@@ -1223,7 +1223,7 @@

Library Stdlib.Lists.List

-

Boolean operations over lists

+

Boolean operations over lists

@@ -1390,7 +1390,7 @@

Library Stdlib.Lists.List

-

Further filtering facts

+

Further filtering facts

@@ -1484,7 +1484,7 @@

Library Stdlib.Lists.List

-

Operations on lists of pairs or lists of lists

+

Operations on lists of pairs or lists of lists

@@ -1616,11 +1616,11 @@

Library Stdlib.Lists.List

-

Miscellaneous operations on lists

+

Miscellaneous operations on lists

-

Length order of lists

+

Length order of lists

@@ -1664,7 +1664,7 @@

Library Stdlib.Lists.List

-

Set inclusion on list

+

Set inclusion on list

@@ -1754,7 +1754,7 @@

Library Stdlib.Lists.List

-

Cutting a list at some position

+

Cutting a list at some position

@@ -1919,7 +1919,7 @@

Library Stdlib.Lists.List

-

Combining pairs of lists of possibly-different lengths

+

Combining pairs of lists of possibly-different lengths

@@ -1951,7 +1951,7 @@

Library Stdlib.Lists.List

-

Predicate for List addition/removal (no need for decidability)

+

Predicate for List addition/removal (no need for decidability)

@@ -1995,7 +1995,7 @@

Library Stdlib.Lists.List

-

Lists without redundancy

+

Lists without redundancy

@@ -2147,7 +2147,7 @@

Library Stdlib.Lists.List

-

Sequence of natural numbers

+

Sequence of natural numbers

@@ -2199,7 +2199,7 @@

Library Stdlib.Lists.List

-

List comparison

+

List comparison

@@ -2336,7 +2336,7 @@

Library Stdlib.Lists.List

-

Existential and universal predicates over lists

+

Existential and universal predicates over lists

@@ -2869,7 +2869,7 @@

Library Stdlib.Lists.List

-

Inversion of predicates over lists based on head symbol

+

Inversion of predicates over lists based on head symbol

@@ -2897,7 +2897,7 @@

Library Stdlib.Lists.List

-

Exporting hints and tactics

+

Exporting hints and tactics

diff --git a/v9.0/stdlib/Stdlib.Lists.SetoidList.html b/v9.0/stdlib/Stdlib.Lists.SetoidList.html index 3482e5bb7f..1ee29d6a73 100644 --- a/v9.0/stdlib/Stdlib.Lists.SetoidList.html +++ b/v9.0/stdlib/Stdlib.Lists.SetoidList.html @@ -52,7 +52,7 @@

Library Stdlib.Lists.SetoidList

-

Logical relations over lists with respect to a setoid equality

+

Logical relations over lists with respect to a setoid equality

or ordering.
diff --git a/v9.0/stdlib/Stdlib.Lists.StreamMemo.html b/v9.0/stdlib/Stdlib.Lists.StreamMemo.html index 2de37f401c..cb3ff9bcb7 100644 --- a/v9.0/stdlib/Stdlib.Lists.StreamMemo.html +++ b/v9.0/stdlib/Stdlib.Lists.StreamMemo.html @@ -52,7 +52,7 @@

Library Stdlib.Lists.StreamMemo

-

Memoization

+

Memoization

diff --git a/v9.0/stdlib/Stdlib.Logic.ChoiceFacts.html b/v9.0/stdlib/Stdlib.Logic.ChoiceFacts.html index d4c56fb03b..64449922fa 100644 --- a/v9.0/stdlib/Stdlib.Logic.ChoiceFacts.html +++ b/v9.0/stdlib/Stdlib.Logic.ChoiceFacts.html @@ -49,7 +49,7 @@

Library Stdlib.Logic.ChoiceFacts

Some facts and definitions concerning choice and description in - intuitionistic logic.

References:

+ intuitionistic logic.

References:

@@ -88,7 +88,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Definitions

+

Definitions

@@ -115,7 +115,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Constructive choice and description

+

Constructive choice and description

@@ -345,7 +345,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Weakly classical choice and description

+

Weakly classical choice and description

@@ -624,7 +624,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Table of contents

+

Table of contents

@@ -681,7 +681,7 @@

Library Stdlib.Logic.ChoiceFacts

-

AC_rel + AC! = AC_fun

+

AC_rel + AC! = AC_fun

@@ -721,7 +721,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Connection between the guarded, non guarded and omniscient choices

+

Connection between the guarded, non guarded and omniscient choices

@@ -732,7 +732,7 @@

Library Stdlib.Logic.ChoiceFacts

irrelevance)
-

AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel

+

AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel

@@ -770,7 +770,7 @@

Library Stdlib.Logic.ChoiceFacts

-

AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker

+

AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker

@@ -845,7 +845,7 @@

Library Stdlib.Logic.ChoiceFacts

-

D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker

+

D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker

@@ -889,7 +889,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Derivability of choice for decidable relations with well-ordered codomain

+

Derivability of choice for decidable relations with well-ordered codomain

@@ -922,11 +922,11 @@

Library Stdlib.Logic.ChoiceFacts

-

AC_fun = AC_fun_dep = AC_trunc

+

AC_fun = AC_fun_dep = AC_trunc

-

Choice on dependent and non dependent function types are equivalent

+

Choice on dependent and non dependent function types are equivalent

@@ -965,7 +965,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Functional choice and truncation choice are equivalent

+

Functional choice and truncation choice are equivalent

@@ -982,7 +982,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Reification of dependent and non dependent functional relation are equivalent

+

Reification of dependent and non dependent functional relation are equivalent

@@ -1017,11 +1017,11 @@

Library Stdlib.Logic.ChoiceFacts

-

Non contradiction of constructive descriptions wrt functional axioms of choice

+

Non contradiction of constructive descriptions wrt functional axioms of choice

-

Non contradiction of indefinite description

+

Non contradiction of indefinite description

@@ -1039,7 +1039,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Non contradiction of definite description

+

Non contradiction of definite description

@@ -1083,7 +1083,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Excluded-middle + definite description => computational excluded-middle

+

Excluded-middle + definite description => computational excluded-middle

@@ -1127,7 +1127,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Choice => Dependent choice => Countable choice

+

Choice => Dependent choice => Countable choice

@@ -1147,7 +1147,7 @@

Library Stdlib.Logic.ChoiceFacts

-

About the axiom of choice over setoids

+

About the axiom of choice over setoids

@@ -1159,7 +1159,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Consequences of the choice of a representative in an equivalence class

+

Consequences of the choice of a representative in an equivalence class

@@ -1180,7 +1180,7 @@

Library Stdlib.Logic.ChoiceFacts

-

This is a variant of Diaconescu and Goodman-Myhill theorems

+

This is a variant of Diaconescu and Goodman-Myhill theorems

@@ -1197,7 +1197,7 @@

Library Stdlib.Logic.ChoiceFacts

-

AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple

+

AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple

@@ -1230,7 +1230,7 @@

Library Stdlib.Logic.ChoiceFacts

-

AC_fun_setoid = AC! + AC_fun_repr

+

AC_fun_setoid = AC! + AC_fun_repr

@@ -1266,7 +1266,7 @@

Library Stdlib.Logic.ChoiceFacts

functional forms, SetoidFunctionalChoice seems strictly stronger
-

AC_fun_setoid = AC_fun + Ext_fun_repr + EM

+

AC_fun_setoid = AC_fun + Ext_fun_repr + EM

@@ -1278,7 +1278,7 @@

Library Stdlib.Logic.ChoiceFacts

-

This is the main theorem in [Carlström04]

+

This is the main theorem in [Carlström04]

@@ -1302,7 +1302,7 @@

Library Stdlib.Logic.ChoiceFacts

-

AC_fun_setoid = AC_fun + Ext_pred_repr + PI

+

AC_fun_setoid = AC_fun + Ext_pred_repr + PI

@@ -1326,7 +1326,7 @@

Library Stdlib.Logic.ChoiceFacts

-

Compatibility notations

+

Compatibility notations

diff --git a/v9.0/stdlib/Stdlib.Logic.ClassicalEpsilon.html b/v9.0/stdlib/Stdlib.Logic.ClassicalEpsilon.html index c80a9725eb..466b7e2a47 100644 --- a/v9.0/stdlib/Stdlib.Logic.ClassicalEpsilon.html +++ b/v9.0/stdlib/Stdlib.Logic.ClassicalEpsilon.html @@ -132,7 +132,7 @@

Library Stdlib.Logic.ClassicalEpsilon

-

Weaker lemmas (compatibility lemmas)

+

Weaker lemmas (compatibility lemmas)

diff --git a/v9.0/stdlib/Stdlib.Logic.ClassicalFacts.html b/v9.0/stdlib/Stdlib.Logic.ClassicalFacts.html index be9f102346..cf71f9bdd0 100644 --- a/v9.0/stdlib/Stdlib.Logic.ClassicalFacts.html +++ b/v9.0/stdlib/Stdlib.Logic.ClassicalFacts.html @@ -117,7 +117,7 @@

Library Stdlib.Logic.ClassicalFacts

-

Prop degeneracy = excluded-middle + prop extensionality

+

Prop degeneracy = excluded-middle + prop extensionality

@@ -193,11 +193,11 @@

Library Stdlib.Logic.ClassicalFacts

-

Classical logic and proof-irrelevance

+

Classical logic and proof-irrelevance

-

CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint

+

CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint

@@ -250,7 +250,7 @@

Library Stdlib.Logic.ClassicalFacts

-

CC |- prop_ext /\ dep elim on bool -> proof-irrelevance

+

CC |- prop_ext /\ dep elim on bool -> proof-irrelevance

@@ -347,7 +347,7 @@

Library Stdlib.Logic.ClassicalFacts

-

CIC |- prop. ext. -> proof-irrelevance

+

CIC |- prop. ext. -> proof-irrelevance

@@ -401,7 +401,7 @@

Library Stdlib.Logic.ClassicalFacts

-

CC |- excluded-middle + dep elim on bool -> proof-irrelevance

+

CC |- excluded-middle + dep elim on bool -> proof-irrelevance

@@ -573,7 +573,7 @@

Library Stdlib.Logic.ClassicalFacts

-

CIC |- excluded-middle -> proof-irrelevance

+

CIC |- excluded-middle -> proof-irrelevance

@@ -638,7 +638,7 @@

Library Stdlib.Logic.ClassicalFacts

-

Weak classical axioms

+

Weak classical axioms

@@ -660,7 +660,7 @@

Library Stdlib.Logic.ClassicalFacts

-

Weak excluded-middle

+

Weak excluded-middle

@@ -715,7 +715,7 @@

Library Stdlib.Logic.ClassicalFacts

-

Gödel-Dummett axiom

+

Gödel-Dummett axiom

@@ -786,7 +786,7 @@

Library Stdlib.Logic.ClassicalFacts

-

Independence of general premises and drinker's paradox

+

Independence of general premises and drinker's paradox

@@ -962,11 +962,11 @@

Library Stdlib.Logic.ClassicalFacts

-

Axioms equivalent to classical logic

+

Axioms equivalent to classical logic

-

Principle of unrestricted minimization

+

Principle of unrestricted minimization

@@ -1039,7 +1039,7 @@

Library Stdlib.Logic.ClassicalFacts

-

Choice of representatives in a partition of bool

+

Choice of representatives in a partition of bool

diff --git a/v9.0/stdlib/Stdlib.Logic.Diaconescu.html b/v9.0/stdlib/Stdlib.Logic.Diaconescu.html index 2559c80aa4..c88f273a79 100644 --- a/v9.0/stdlib/Stdlib.Logic.Diaconescu.html +++ b/v9.0/stdlib/Stdlib.Logic.Diaconescu.html @@ -107,7 +107,7 @@

Library Stdlib.Logic.Diaconescu

-

Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle

+

Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle

@@ -203,7 +203,7 @@

Library Stdlib.Logic.Diaconescu

-

Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality

+

Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality

@@ -310,7 +310,7 @@

Library Stdlib.Logic.Diaconescu

-

Extensional Hilbert's epsilon description operator -> Excluded-Middle

+

Extensional Hilbert's epsilon description operator -> Excluded-Middle

diff --git a/v9.0/stdlib/Stdlib.Logic.EqdepFacts.html b/v9.0/stdlib/Stdlib.Logic.EqdepFacts.html index 524f0f0660..1036d2b7a3 100644 --- a/v9.0/stdlib/Stdlib.Logic.EqdepFacts.html +++ b/v9.0/stdlib/Stdlib.Logic.EqdepFacts.html @@ -115,7 +115,7 @@

Library Stdlib.Logic.EqdepFacts

-

Definition of dependent equality and equivalence with equality of dependent pairs

+

Definition of dependent equality and equivalence with equality of dependent pairs

@@ -283,7 +283,7 @@

Library Stdlib.Logic.EqdepFacts

-

Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K

+

Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K

@@ -509,7 +509,7 @@

Library Stdlib.Logic.EqdepFacts

-

Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq

+

Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq

diff --git a/v9.0/stdlib/Stdlib.Logic.Eqdep_dec.html b/v9.0/stdlib/Stdlib.Logic.Eqdep_dec.html index 86b4ef91ba..0e1a622aad 100644 --- a/v9.0/stdlib/Stdlib.Logic.Eqdep_dec.html +++ b/v9.0/stdlib/Stdlib.Logic.Eqdep_dec.html @@ -87,7 +87,7 @@

Library Stdlib.Logic.Eqdep_dec

-

Streicher's K and injectivity of dependent pair hold on decidable types

+

Streicher's K and injectivity of dependent pair hold on decidable types

@@ -245,7 +245,7 @@

Library Stdlib.Logic.Eqdep_dec

-

Definition of the functor that builds properties of dependent equalities on decidable sets in Type

+

Definition of the functor that builds properties of dependent equalities on decidable sets in Type

@@ -369,7 +369,7 @@

Library Stdlib.Logic.Eqdep_dec

-

Definition of the functor that builds properties of dependent equalities on decidable sets in Set

+

Definition of the functor that builds properties of dependent equalities on decidable sets in Set

diff --git a/v9.0/stdlib/Stdlib.Logic.ExtensionalityFacts.html b/v9.0/stdlib/Stdlib.Logic.ExtensionalityFacts.html index 4b253f7424..8b7cd6cf9e 100644 --- a/v9.0/stdlib/Stdlib.Logic.ExtensionalityFacts.html +++ b/v9.0/stdlib/Stdlib.Logic.ExtensionalityFacts.html @@ -104,7 +104,7 @@

Library Stdlib.Logic.ExtensionalityFacts

-

Definitions

+

Definitions

@@ -196,7 +196,7 @@

Library Stdlib.Logic.ExtensionalityFacts

-

Functional extensionality <-> Equality of projections from diagonal

+

Functional extensionality <-> Equality of projections from diagonal

@@ -208,7 +208,7 @@

Library Stdlib.Logic.ExtensionalityFacts

-

Functional extensionality <-> Unicity of bijection inverse

+

Functional extensionality <-> Unicity of bijection inverse

@@ -226,7 +226,7 @@

Library Stdlib.Logic.ExtensionalityFacts

-

Functional extensionality <-> Bijectivity of bijective composition

+

Functional extensionality <-> Bijectivity of bijective composition

diff --git a/v9.0/stdlib/Stdlib.Logic.FinFun.html b/v9.0/stdlib/Stdlib.Logic.FinFun.html index dcda66c34b..1ae377f9e0 100644 --- a/v9.0/stdlib/Stdlib.Logic.FinFun.html +++ b/v9.0/stdlib/Stdlib.Logic.FinFun.html @@ -48,7 +48,7 @@

Library Stdlib.Logic.FinFun

-

Functions on finite domains

+

Functions on finite domains

diff --git a/v9.0/stdlib/Stdlib.Logic.Hurkens.html b/v9.0/stdlib/Stdlib.Logic.Hurkens.html index 83296166e8..1e267df946 100644 --- a/v9.0/stdlib/Stdlib.Logic.Hurkens.html +++ b/v9.0/stdlib/Stdlib.Logic.Hurkens.html @@ -175,7 +175,7 @@

Library Stdlib.Logic.Hurkens

-

A modular proof of Hurkens's paradox.

+

A modular proof of Hurkens's paradox.

@@ -202,7 +202,7 @@

Library Stdlib.Logic.Hurkens

-

Axiomatisation of impredicative universes in a Martin-Löf style

+

Axiomatisation of impredicative universes in a Martin-Löf style

@@ -213,7 +213,7 @@

Library Stdlib.Logic.Hurkens

actual system U-.
-

Large universe

+

Large universe

@@ -222,7 +222,7 @@

Library Stdlib.Logic.Hurkens

-

Closure by small product

+

Closure by small product

@@ -238,7 +238,7 @@

Library Stdlib.Logic.Hurkens

-

Closure by large products

+

Closure by large products

U1 only needs to quantify over itself.
@@ -255,7 +255,7 @@

Library Stdlib.Logic.Hurkens

-

Small universe

+

Small universe

The small universe is an element of the large one.
@@ -265,7 +265,7 @@

Library Stdlib.Logic.Hurkens

-

Closure by small product

+

Closure by small product

U0 does not need reduction rules
@@ -279,7 +279,7 @@

Library Stdlib.Logic.Hurkens

-

Closure by large products

+

Closure by large products

@@ -294,7 +294,7 @@

Library Stdlib.Logic.Hurkens

-

Automating the rewrite rules of our encoding.

+

Automating the rewrite rules of our encoding.

@@ -312,7 +312,7 @@

Library Stdlib.Logic.Hurkens

-

Hurkens's paradox.

+

Hurkens's paradox.

@@ -325,7 +325,7 @@

Library Stdlib.Logic.Hurkens

-

Preliminary definitions

+

Preliminary definitions

@@ -354,7 +354,7 @@

Library Stdlib.Logic.Hurkens

-

Proof

+

Proof

@@ -439,7 +439,7 @@

Library Stdlib.Logic.Hurkens

-

Impredicative universes are not retracts.

+

Impredicative universes are not retracts.

@@ -466,7 +466,7 @@

Library Stdlib.Logic.Hurkens

-

U1 is impredicative

+

U1 is impredicative

@@ -493,7 +493,7 @@

Library Stdlib.Logic.Hurkens

-

U0 is a retract of U1

+

U0 is a retract of U1

@@ -506,7 +506,7 @@

Library Stdlib.Logic.Hurkens

-

Paradox

+

Paradox

@@ -570,7 +570,7 @@

Library Stdlib.Logic.Hurkens

-

Modal fragments of Prop are not retracts

+

Modal fragments of Prop are not retracts

@@ -589,7 +589,7 @@

Library Stdlib.Logic.Hurkens

-

Monadic modality

+

Monadic modality

@@ -612,7 +612,7 @@

Library Stdlib.Logic.Hurkens

-

The universe of modal propositions

+

The universe of modal propositions

@@ -642,7 +642,7 @@

Library Stdlib.Logic.Hurkens

-

Retract of the modal fragment of Prop in a small type

+

Retract of the modal fragment of Prop in a small type

@@ -662,7 +662,7 @@

Library Stdlib.Logic.Hurkens

-

Paradox

+

Paradox

@@ -721,7 +721,7 @@

Library Stdlib.Logic.Hurkens

-

The negative fragment of Prop is not a retract

+

The negative fragment of Prop is not a retract

@@ -738,7 +738,7 @@

Library Stdlib.Logic.Hurkens

-

The universe of negative propositions.

+

The universe of negative propositions.

@@ -754,7 +754,7 @@

Library Stdlib.Logic.Hurkens

-

Retract of the negative fragment of Prop in a small type

+

Retract of the negative fragment of Prop in a small type

@@ -774,7 +774,7 @@

Library Stdlib.Logic.Hurkens

-

Paradox

+

Paradox

@@ -805,7 +805,7 @@

Library Stdlib.Logic.Hurkens

-

Prop is not a retract

+

Prop is not a retract

@@ -822,7 +822,7 @@

Library Stdlib.Logic.Hurkens

-

The universe of propositions.

+

The universe of propositions.

@@ -838,7 +838,7 @@

Library Stdlib.Logic.Hurkens

-

Retract of Prop in a small type, using the identity modality.

+

Retract of Prop in a small type, using the identity modality.

@@ -854,7 +854,7 @@

Library Stdlib.Logic.Hurkens

-

Paradox

+

Paradox

@@ -885,7 +885,7 @@

Library Stdlib.Logic.Hurkens

-

Retract of Prop in a small type

+

Retract of Prop in a small type

@@ -903,7 +903,7 @@

Library Stdlib.Logic.Hurkens

-

Paradox

+

Paradox

@@ -930,7 +930,7 @@

Library Stdlib.Logic.Hurkens

-

Large universes are not retracts of Prop.

+

Large universes are not retracts of Prop.

@@ -955,7 +955,7 @@

Library Stdlib.Logic.Hurkens

-

Assumption of a retract from Type into Prop

+

Assumption of a retract from Type into Prop

@@ -969,7 +969,7 @@

Library Stdlib.Logic.Hurkens

-

Paradox

+

Paradox

@@ -1024,7 +1024,7 @@

Library Stdlib.Logic.Hurkens

-

A<>Type

+

A<>Type

@@ -1045,7 +1045,7 @@

Library Stdlib.Logic.Hurkens

-

Universe U is equal to one of its elements.

+

Universe U is equal to one of its elements.

@@ -1059,7 +1059,7 @@

Library Stdlib.Logic.Hurkens

-

Universe U is a retract of A

+

Universe U is a retract of A

@@ -1149,7 +1149,7 @@

Library Stdlib.Logic.Hurkens

-

Prop<>Type.

+

Prop<>Type.

diff --git a/v9.0/stdlib/Stdlib.Logic.PropExtensionalityFacts.html b/v9.0/stdlib/Stdlib.Logic.PropExtensionalityFacts.html index 747a9cde50..ba666ee9fa 100644 --- a/v9.0/stdlib/Stdlib.Logic.PropExtensionalityFacts.html +++ b/v9.0/stdlib/Stdlib.Logic.PropExtensionalityFacts.html @@ -116,7 +116,7 @@

Library Stdlib.Logic.PropExtensionalityFacts

-

Definitions

+

Definitions

@@ -180,11 +180,11 @@

Library Stdlib.Logic.PropExtensionalityFacts

-

Propositional and predicate extensionality

+

Propositional and predicate extensionality

-

Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality

+

Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality

@@ -207,7 +207,7 @@

Library Stdlib.Logic.PropExtensionalityFacts

-

Propositional extensionality and provable proposition extensionality

+

Propositional extensionality and provable proposition extensionality

@@ -219,7 +219,7 @@

Library Stdlib.Logic.PropExtensionalityFacts

-

Propositional extensionality and refutable proposition extensionality

+

Propositional extensionality and refutable proposition extensionality

diff --git a/v9.0/stdlib/Stdlib.Logic.PropFacts.html b/v9.0/stdlib/Stdlib.Logic.PropFacts.html index 71acffa0a2..eff5570671 100644 --- a/v9.0/stdlib/Stdlib.Logic.PropFacts.html +++ b/v9.0/stdlib/Stdlib.Logic.PropFacts.html @@ -48,7 +48,7 @@

Library Stdlib.Logic.PropFacts

-

Basic facts about Prop as a type

+

Basic facts about Prop as a type

diff --git a/v9.0/stdlib/Stdlib.Logic.SetIsType.html b/v9.0/stdlib/Stdlib.Logic.SetIsType.html index e0a0bba750..51e960e3fb 100644 --- a/v9.0/stdlib/Stdlib.Logic.SetIsType.html +++ b/v9.0/stdlib/Stdlib.Logic.SetIsType.html @@ -48,7 +48,7 @@

Library Stdlib.Logic.SetIsType

-

The Set universe seen as a synonym for Type

+

The Set universe seen as a synonym for Type

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetAVL.html b/v9.0/stdlib/Stdlib.MSets.MSetAVL.html index a38ab60671..81e34ad41a 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetAVL.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetAVL.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetAVL

-

MSetAVL : Implementation of MSetInterface via AVL trees

+

MSetAVL : Implementation of MSetInterface via AVL trees

@@ -90,7 +90,7 @@

Library Stdlib.MSets.MSetAVL

-

Ops : the pure functions

+

Ops : the pure functions

@@ -104,7 +104,7 @@

Library Stdlib.MSets.MSetAVL

-

Generic trees instantiated with integer height

+

Generic trees instantiated with integer height

@@ -124,7 +124,7 @@

Library Stdlib.MSets.MSetAVL

-

Height of trees

+

Height of trees

@@ -140,7 +140,7 @@

Library Stdlib.MSets.MSetAVL

-

Singleton set

+

Singleton set

@@ -152,7 +152,7 @@

Library Stdlib.MSets.MSetAVL

-

Helper functions

+

Helper functions

@@ -215,7 +215,7 @@

Library Stdlib.MSets.MSetAVL

-

Insertion

+

Insertion

@@ -235,7 +235,7 @@

Library Stdlib.MSets.MSetAVL

-

Join

+

Join

@@ -264,7 +264,7 @@

Library Stdlib.MSets.MSetAVL

-

Extraction of minimum element

+

Extraction of minimum element

@@ -288,7 +288,7 @@

Library Stdlib.MSets.MSetAVL

-

Merging two trees

+

Merging two trees

@@ -312,7 +312,7 @@

Library Stdlib.MSets.MSetAVL

-

Deletion

+

Deletion

@@ -332,7 +332,7 @@

Library Stdlib.MSets.MSetAVL

-

Concatenation

+

Concatenation

@@ -356,7 +356,7 @@

Library Stdlib.MSets.MSetAVL

-

Splitting

+

Splitting

@@ -396,7 +396,7 @@

Library Stdlib.MSets.MSetAVL

-

Intersection

+

Intersection

@@ -415,7 +415,7 @@

Library Stdlib.MSets.MSetAVL

-

Difference

+

Difference

@@ -434,7 +434,7 @@

Library Stdlib.MSets.MSetAVL

-

Union

+

Union

@@ -465,7 +465,7 @@

Library Stdlib.MSets.MSetAVL

-

Filter

+

Filter

@@ -483,7 +483,7 @@

Library Stdlib.MSets.MSetAVL

-

Partition

+

Partition

@@ -506,7 +506,7 @@

Library Stdlib.MSets.MSetAVL

-

MakeRaw

+

MakeRaw

@@ -779,7 +779,7 @@

Library Stdlib.MSets.MSetAVL

-

Singleton set

+

Singleton set

@@ -795,7 +795,7 @@

Library Stdlib.MSets.MSetAVL

-

Helper functions

+

Helper functions

@@ -822,7 +822,7 @@

Library Stdlib.MSets.MSetAVL

-

Insertion

+

Insertion

@@ -846,7 +846,7 @@

Library Stdlib.MSets.MSetAVL

-

Join

+

Join

@@ -885,7 +885,7 @@

Library Stdlib.MSets.MSetAVL

-

Extraction of minimum element

+

Extraction of minimum element

@@ -909,7 +909,7 @@

Library Stdlib.MSets.MSetAVL

-

Merging two trees

+

Merging two trees

@@ -928,7 +928,7 @@

Library Stdlib.MSets.MSetAVL

-

Deletion

+

Deletion

@@ -945,7 +945,7 @@

Library Stdlib.MSets.MSetAVL

-

Concatenation

+

Concatenation

@@ -964,7 +964,7 @@

Library Stdlib.MSets.MSetAVL

-

Splitting

+

Splitting

@@ -996,7 +996,7 @@

Library Stdlib.MSets.MSetAVL

-

Intersection

+

Intersection

@@ -1026,7 +1026,7 @@

Library Stdlib.MSets.MSetAVL

-

Difference

+

Difference

@@ -1047,7 +1047,7 @@

Library Stdlib.MSets.MSetAVL

-

Union

+

Union

@@ -1064,7 +1064,7 @@

Library Stdlib.MSets.MSetAVL

-

Filter

+

Filter

@@ -1086,7 +1086,7 @@

Library Stdlib.MSets.MSetAVL

-

Partition

+

Partition

@@ -1123,7 +1123,7 @@

Library Stdlib.MSets.MSetAVL

-

Encapsulation

+

Encapsulation

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetDecide.html b/v9.0/stdlib/Stdlib.MSets.MSetDecide.html index f865d82c3e..5bd3894e69 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetDecide.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetDecide.html @@ -74,7 +74,7 @@

Library Stdlib.MSets.MSetDecide

-

Overview

+

Overview

This functor defines the tactic fsetdec, which will solve any valid goal of the form @@ -180,7 +180,7 @@

Library Stdlib.MSets.MSetDecide

-

Facts and Tactics for Propositional Logic

+

Facts and Tactics for Propositional Logic

These lemmas and tactics are in a module so that they do not affect the namespace if you import the enclosing @@ -195,18 +195,18 @@

Library Stdlib.MSets.MSetDecide

-

Lemmas and Tactics About Decidable Propositions

+

Lemmas and Tactics About Decidable Propositions

-

Propositional Equivalences Involving Negation

+

Propositional Equivalences Involving Negation

These are all written with the unfolded form of negation, since I am not sure if setoid rewriting will always perform conversion.
-

Tactics for Negations

+

Tactics for Negations

@@ -457,7 +457,7 @@

Library Stdlib.MSets.MSetDecide

-

Auxiliary Tactics

+

Auxiliary Tactics

Again, these lemmas and tactics are in a module so that they do not affect the namespace if you import the @@ -470,7 +470,7 @@

Library Stdlib.MSets.MSetDecide

-

Generic Tactics

+

Generic Tactics

We begin by defining a few generic, useful tactics.
@@ -587,7 +587,7 @@

Library Stdlib.MSets.MSetDecide

-

Discarding Irrelevant Hypotheses

+

Discarding Irrelevant Hypotheses

We will want to clear the context of any non-MSet-related hypotheses in order to increase the @@ -667,7 +667,7 @@

Library Stdlib.MSets.MSetDecide

-

Turning Set Operators into Propositional Connectives

+

Turning Set Operators into Propositional Connectives

The lemmas from MSetFacts will be used to break down set operations into propositional formulas built over @@ -693,7 +693,7 @@

Library Stdlib.MSets.MSetDecide

-

Decidability of MSet Propositions

+

Decidability of MSet Propositions

@@ -728,7 +728,7 @@

Library Stdlib.MSets.MSetDecide

-

Normalizing Propositions About Equality

+

Normalizing Propositions About Equality

We have to deal with the fact that E.eq may be convertible with Coq's equality. Thus, we will find the @@ -811,7 +811,7 @@

Library Stdlib.MSets.MSetDecide

-

Considering Decidability of Base Propositions

+

Considering Decidability of Base Propositions

This tactic adds assertions about the decidability of E.eq and In to the context. This is necessary for @@ -860,7 +860,7 @@

Library Stdlib.MSets.MSetDecide

-

Handling Empty, Subset, and Equal

+

Handling Empty, Subset, and Equal

This tactic instantiates universally quantified hypotheses (which arise from the unfolding of Empty, @@ -908,7 +908,7 @@

Library Stdlib.MSets.MSetDecide

-

The Core fsetdec Auxiliary Tactics

+

The Core fsetdec Auxiliary Tactics

@@ -950,7 +950,7 @@

Library Stdlib.MSets.MSetDecide

-

The fsetdec Tactic

+

The fsetdec Tactic

Here is the top-level tactic (the only one intended for clients of this library). It's specification is given at @@ -1064,7 +1064,7 @@

Library Stdlib.MSets.MSetDecide

-

Examples

+

Examples

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetEqProperties.html b/v9.0/stdlib/Stdlib.MSets.MSetEqProperties.html index 39b820e6ca..7631040b98 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetEqProperties.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetEqProperties.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetEqProperties

-

Finite sets library

+

Finite sets library

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetFacts.html b/v9.0/stdlib/Stdlib.MSets.MSetFacts.html index 9f357adb8c..931e30112d 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetFacts.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetFacts.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetFacts

-

Finite sets library

+

Finite sets library

@@ -87,7 +87,7 @@

Library Stdlib.MSets.MSetFacts

-

Specifications written using implications :

+

Specifications written using implications :

this used to be the default interface.
@@ -204,7 +204,7 @@

Library Stdlib.MSets.MSetFacts

-

Specifications written using equivalences :

+

Specifications written using equivalences :

this is now provided by the default interface.
@@ -293,7 +293,7 @@

Library Stdlib.MSets.MSetFacts

-

Specifications written using boolean predicates

+

Specifications written using boolean predicates

@@ -357,7 +357,7 @@

Library Stdlib.MSets.MSetFacts

-

Declarations of morphisms with respects to E.eq and Equal

+

Declarations of morphisms with respects to E.eq and Equal

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetGenTree.html b/v9.0/stdlib/Stdlib.MSets.MSetGenTree.html index 50c66be959..ef8782388c 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetGenTree.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetGenTree.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetGenTree

-

MSetGenTree : sets via generic trees

+

MSetGenTree : sets via generic trees

@@ -106,7 +106,7 @@

Library Stdlib.MSets.MSetGenTree

-

Ops : the pure functions

+

Ops : the pure functions

@@ -128,7 +128,7 @@

Library Stdlib.MSets.MSetGenTree

-

The empty set and emptyness test

+

The empty set and emptyness test

@@ -147,7 +147,7 @@

Library Stdlib.MSets.MSetGenTree

-

Membership test

+

Membership test

@@ -172,7 +172,7 @@

Library Stdlib.MSets.MSetGenTree

-

Minimal, maximal, arbitrary elements

+

Minimal, maximal, arbitrary elements

@@ -200,7 +200,7 @@

Library Stdlib.MSets.MSetGenTree

-

Iteration on elements

+

Iteration on elements

@@ -257,7 +257,7 @@

Library Stdlib.MSets.MSetGenTree

-

Testing universal or existential properties.

+

Testing universal or existential properties.

@@ -282,7 +282,7 @@

Library Stdlib.MSets.MSetGenTree

-

Comparison of trees

+

Comparison of trees

@@ -389,7 +389,7 @@

Library Stdlib.MSets.MSetGenTree

-

Subset test

+

Subset test

@@ -448,7 +448,7 @@

Library Stdlib.MSets.MSetGenTree

-

Props : correctness proofs of these generic operations

+

Props : correctness proofs of these generic operations

@@ -460,7 +460,7 @@

Library Stdlib.MSets.MSetGenTree

-

Occurrence in a tree

+

Occurrence in a tree

@@ -478,7 +478,7 @@

Library Stdlib.MSets.MSetGenTree

-

Some shortcuts

+

Some shortcuts

@@ -494,7 +494,7 @@

Library Stdlib.MSets.MSetGenTree

-

Binary search trees

+

Binary search trees

@@ -572,7 +572,7 @@

Library Stdlib.MSets.MSetGenTree

-

Known facts about ordered types

+

Known facts about ordered types

@@ -584,7 +584,7 @@

Library Stdlib.MSets.MSetGenTree

-

Automation and dedicated tactics

+

Automation and dedicated tactics

@@ -691,7 +691,7 @@

Library Stdlib.MSets.MSetGenTree

-

Basic results about In

+

Basic results about In

@@ -789,7 +789,7 @@

Library Stdlib.MSets.MSetGenTree

-

Empty set

+

Empty set

@@ -805,7 +805,7 @@

Library Stdlib.MSets.MSetGenTree

-

Emptyness test

+

Emptyness test

@@ -817,7 +817,7 @@

Library Stdlib.MSets.MSetGenTree

-

Membership

+

Membership

@@ -829,7 +829,7 @@

Library Stdlib.MSets.MSetGenTree

-

Minimal and maximal elements

+

Minimal and maximal elements

@@ -869,7 +869,7 @@

Library Stdlib.MSets.MSetGenTree

-

Elements

+

Elements

@@ -945,7 +945,7 @@

Library Stdlib.MSets.MSetGenTree

-

for_all and exists

+

for_all and exists

@@ -962,7 +962,7 @@

Library Stdlib.MSets.MSetGenTree

-

Fold

+

Fold

@@ -979,7 +979,7 @@

Library Stdlib.MSets.MSetGenTree

-

Subset

+

Subset

@@ -1004,7 +1004,7 @@

Library Stdlib.MSets.MSetGenTree

-

Comparison

+

Comparison

@@ -1106,7 +1106,7 @@

Library Stdlib.MSets.MSetGenTree

-

Equality test

+

Equality test

@@ -1119,7 +1119,7 @@

Library Stdlib.MSets.MSetGenTree

-

A few results about mindepth and maxdepth

+

A few results about mindepth and maxdepth

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetInterface.html b/v9.0/stdlib/Stdlib.MSets.MSetInterface.html index 47405b0fe7..cc4e8fde6d 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetInterface.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetInterface.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetInterface

-

Finite set library

+

Finite set library

@@ -317,7 +317,7 @@

Library Stdlib.MSets.MSetInterface

-

Functorial signature for weak sets

+

Functorial signature for weak sets

@@ -431,7 +431,7 @@

Library Stdlib.MSets.MSetInterface

-

Static signature for weak sets

+

Static signature for weak sets

@@ -451,7 +451,7 @@

Library Stdlib.MSets.MSetInterface

-

Functorial signature for sets on ordered elements

+

Functorial signature for sets on ordered elements

@@ -563,7 +563,7 @@

Library Stdlib.MSets.MSetInterface

-

Static signature for sets on ordered elements

+

Static signature for sets on ordered elements

@@ -586,7 +586,7 @@

Library Stdlib.MSets.MSetInterface

-

Some subtyping tests

+

Some subtyping tests

 WSetsOn ---> WSets
@@ -603,7 +603,7 @@ 
Library Stdlib.MSets.MSetInterface

 
 
 

 
-
Signatures for set representations with ill-formed values.

+
Signatures for set representations with ill-formed values.

 
 
 
 

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetList.html b/v9.0/stdlib/Stdlib.MSets.MSetList.html
index 3cfdd20b7a..4f5343d06e 100644
--- a/v9.0/stdlib/Stdlib.MSets.MSetList.html
+++ b/v9.0/stdlib/Stdlib.MSets.MSetList.html
@@ -48,7 +48,7 @@ 
Library Stdlib.MSets.MSetList
-

Finite sets library

+

Finite sets library

@@ -65,7 +65,7 @@

Library Stdlib.MSets.MSetList

-

Functions over lists

+

Functions over lists

@@ -93,7 +93,7 @@

Library Stdlib.MSets.MSetList

-

The set operations.

+

The set operations.

@@ -301,7 +301,7 @@

Library Stdlib.MSets.MSetList

-

Proofs of set operation specifications.

+

Proofs of set operation specifications.

@@ -642,7 +642,7 @@

Library Stdlib.MSets.MSetList

-

Encapsulation

+

Encapsulation

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetProperties.html b/v9.0/stdlib/Stdlib.MSets.MSetProperties.html index 0a67345b7f..e6b65a2886 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetProperties.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetProperties.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetProperties

-

Finite sets library

+

Finite sets library

@@ -341,7 +341,7 @@

Library Stdlib.MSets.MSetProperties

-

Properties of elements

+

Properties of elements

@@ -356,7 +356,7 @@

Library Stdlib.MSets.MSetProperties

-

Conversions between lists and sets

+

Conversions between lists and sets

@@ -380,7 +380,7 @@

Library Stdlib.MSets.MSetProperties

-

Fold

+

Fold

@@ -408,7 +408,7 @@

Library Stdlib.MSets.MSetProperties

-

Induction principles for fold (contributed by S. Lescuyer)

+

Induction principles for fold (contributed by S. Lescuyer)

@@ -514,7 +514,7 @@

Library Stdlib.MSets.MSetProperties

-

Alternative (weaker) specifications for fold

+

Alternative (weaker) specifications for fold

@@ -586,7 +586,7 @@

Library Stdlib.MSets.MSetProperties

-

Fold is a morphism

+

Fold is a morphism

@@ -603,7 +603,7 @@

Library Stdlib.MSets.MSetProperties

-

Fold and other set operators

+

Fold and other set operators

@@ -655,11 +655,11 @@

Library Stdlib.MSets.MSetProperties

-

Cardinal

+

Cardinal

-

Characterization of cardinal in terms of fold

+

Characterization of cardinal in terms of fold

@@ -671,7 +671,7 @@

Library Stdlib.MSets.MSetProperties

-

Old specifications for cardinal.

+

Old specifications for cardinal.

@@ -694,7 +694,7 @@

Library Stdlib.MSets.MSetProperties

-

Cardinal and (non-)emptiness

+

Cardinal and (non-)emptiness

@@ -719,7 +719,7 @@

Library Stdlib.MSets.MSetProperties

-

Cardinal is a morphism

+

Cardinal is a morphism

@@ -739,7 +739,7 @@

Library Stdlib.MSets.MSetProperties

-

Cardinal and set operators

+

Cardinal and set operators

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetRBT.html b/v9.0/stdlib/Stdlib.MSets.MSetRBT.html index 360c2067a0..ae288a84ad 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetRBT.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetRBT.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetRBT

-

MSetRBT : Implementation of MSetInterface via Red-Black trees

+

MSetRBT : Implementation of MSetInterface via Red-Black trees

@@ -152,7 +152,7 @@

Library Stdlib.MSets.MSetRBT

-

Ops : the pure functions

+

Ops : the pure functions

@@ -164,7 +164,7 @@

Library Stdlib.MSets.MSetRBT

-

Generic trees instantiated with color

+

Generic trees instantiated with color

@@ -186,7 +186,7 @@

Library Stdlib.MSets.MSetRBT

-

Basic tree

+

Basic tree

@@ -198,7 +198,7 @@

Library Stdlib.MSets.MSetRBT

-

Changing root color

+

Changing root color

@@ -221,7 +221,7 @@

Library Stdlib.MSets.MSetRBT

-

Balancing

+

Balancing

@@ -302,7 +302,7 @@

Library Stdlib.MSets.MSetRBT

-

Insertion

+

Insertion

@@ -334,7 +334,7 @@

Library Stdlib.MSets.MSetRBT

-

Deletion

+

Deletion

@@ -394,7 +394,7 @@

Library Stdlib.MSets.MSetRBT

-

Removing minimal element

+

Removing minimal element

@@ -424,7 +424,7 @@

Library Stdlib.MSets.MSetRBT

-

Tree-ification

+

Tree-ification

@@ -487,7 +487,7 @@

Library Stdlib.MSets.MSetRBT

-

Filtering

+

Filtering

@@ -525,7 +525,7 @@

Library Stdlib.MSets.MSetRBT

-

Union, intersection, difference

+

Union, intersection, difference

@@ -685,7 +685,7 @@

Library Stdlib.MSets.MSetRBT

-

MakeRaw : the pure functions and their specifications

+

MakeRaw : the pure functions and their specifications

@@ -723,7 +723,7 @@

Library Stdlib.MSets.MSetRBT

-

Singleton set

+

Singleton set

@@ -739,7 +739,7 @@

Library Stdlib.MSets.MSetRBT

-

makeBlack, MakeRed

+

makeBlack, MakeRed

@@ -762,7 +762,7 @@

Library Stdlib.MSets.MSetRBT

-

Generic handling for red-matching and red-red-matching

+

Generic handling for red-matching and red-red-matching

@@ -887,7 +887,7 @@

Library Stdlib.MSets.MSetRBT

-

Balancing for insertion

+

Balancing for insertion

@@ -933,7 +933,7 @@

Library Stdlib.MSets.MSetRBT

-

Insertion

+

Insertion

@@ -966,7 +966,7 @@

Library Stdlib.MSets.MSetRBT

-

Balancing for deletion

+

Balancing for deletion

@@ -996,7 +996,7 @@

Library Stdlib.MSets.MSetRBT

-

Append for deletion

+

Append for deletion

@@ -1049,7 +1049,7 @@

Library Stdlib.MSets.MSetRBT

-

Deletion

+

Deletion

@@ -1080,7 +1080,7 @@

Library Stdlib.MSets.MSetRBT

-

Removing the minimal element

+

Removing the minimal element

@@ -1109,7 +1109,7 @@

Library Stdlib.MSets.MSetRBT

-

Treeify

+

Treeify

@@ -1161,7 +1161,7 @@

Library Stdlib.MSets.MSetRBT

-

Filter

+

Filter

@@ -1187,7 +1187,7 @@

Library Stdlib.MSets.MSetRBT

-

Partition

+

Partition

@@ -1223,7 +1223,7 @@

Library Stdlib.MSets.MSetRBT

-

An invariant for binary list functions with accumulator.

+

An invariant for binary list functions with accumulator.

@@ -1270,7 +1270,7 @@

Library Stdlib.MSets.MSetRBT

-

union

+

union

@@ -1318,7 +1318,7 @@

Library Stdlib.MSets.MSetRBT

-

inter

+

inter

@@ -1359,7 +1359,7 @@

Library Stdlib.MSets.MSetRBT

-

difference

+

difference

@@ -1408,7 +1408,7 @@

Library Stdlib.MSets.MSetRBT

-

Balancing properties

+

Balancing properties

@@ -1431,7 +1431,7 @@

Library Stdlib.MSets.MSetRBT

-

Red-Black invariants

+

Red-Black invariants

@@ -1502,7 +1502,7 @@

Library Stdlib.MSets.MSetRBT

-

Basic tactics and results about red-black

+

Basic tactics and results about red-black

@@ -1537,7 +1537,7 @@

Library Stdlib.MSets.MSetRBT

-

A Red-Black tree has indeed a logarithmic depth

+

A Red-Black tree has indeed a logarithmic depth

@@ -1563,7 +1563,7 @@

Library Stdlib.MSets.MSetRBT

-

Singleton

+

Singleton

@@ -1575,7 +1575,7 @@

Library Stdlib.MSets.MSetRBT

-

makeBlack and makeRed

+

makeBlack and makeRed

@@ -1591,7 +1591,7 @@

Library Stdlib.MSets.MSetRBT

-

Balancing

+

Balancing

@@ -1628,7 +1628,7 @@

Library Stdlib.MSets.MSetRBT

-

Insertion

+

Insertion

@@ -1661,7 +1661,7 @@

Library Stdlib.MSets.MSetRBT

-

Deletion

+

Deletion

@@ -1692,7 +1692,7 @@

Library Stdlib.MSets.MSetRBT

-

Treeify

+

Treeify

@@ -1739,7 +1739,7 @@

Library Stdlib.MSets.MSetRBT

-

Filtering

+

Filtering

@@ -1760,7 +1760,7 @@

Library Stdlib.MSets.MSetRBT

-

Union, intersection, difference

+

Union, intersection, difference

@@ -1789,7 +1789,7 @@

Library Stdlib.MSets.MSetRBT

-

Final Encapsulation

+

Final Encapsulation

diff --git a/v9.0/stdlib/Stdlib.MSets.MSetToFiniteSet.html b/v9.0/stdlib/Stdlib.MSets.MSetToFiniteSet.html index 9733dbc4d4..2a2b248e4b 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetToFiniteSet.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetToFiniteSet.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetToFiniteSet

-

Finite sets library : conversion to old Finite_sets

+

Finite sets library : conversion to old Finite_sets

@@ -61,7 +61,7 @@

Library Stdlib.MSets.MSetToFiniteSet

-

Going from MSets with usual Leibniz equality

+

Going from MSets with usual Leibniz equality

to the good old Ensembles and Finite_sets theory.
diff --git a/v9.0/stdlib/Stdlib.MSets.MSetWeakList.html b/v9.0/stdlib/Stdlib.MSets.MSetWeakList.html index 001f3c8957..d1702af946 100644 --- a/v9.0/stdlib/Stdlib.MSets.MSetWeakList.html +++ b/v9.0/stdlib/Stdlib.MSets.MSetWeakList.html @@ -48,7 +48,7 @@

Library Stdlib.MSets.MSetWeakList

-

Finite sets library

+

Finite sets library

@@ -68,7 +68,7 @@

Library Stdlib.MSets.MSetWeakList

-

Functions over lists

+

Functions over lists

@@ -78,7 +78,7 @@

Library Stdlib.MSets.MSetWeakList

And the functions returning sets are proved to preserve this invariant.
-

The set operations.

+

The set operations.

@@ -193,7 +193,7 @@

Library Stdlib.MSets.MSetWeakList

-

Proofs of set operation specifications.

+

Proofs of set operation specifications.

@@ -425,7 +425,7 @@

Library Stdlib.MSets.MSetWeakList

-

Encapsulation

+

Encapsulation

diff --git a/v9.0/stdlib/Stdlib.NArith.BinNat.html b/v9.0/stdlib/Stdlib.NArith.BinNat.html index 434e55add8..c967b43bb7 100644 --- a/v9.0/stdlib/Stdlib.NArith.BinNat.html +++ b/v9.0/stdlib/Stdlib.NArith.BinNat.html @@ -54,7 +54,7 @@

Library Stdlib.NArith.BinNat

-

Binary natural numbers, operations and properties

+

Binary natural numbers, operations and properties

@@ -894,7 +894,7 @@

Library Stdlib.NArith.BinNat

-

Properties of iter

+

Properties of iter

diff --git a/v9.0/stdlib/Stdlib.NArith.BinNatDef.html b/v9.0/stdlib/Stdlib.NArith.BinNatDef.html index 8648319cd7..5f27d1df8f 100644 --- a/v9.0/stdlib/Stdlib.NArith.BinNatDef.html +++ b/v9.0/stdlib/Stdlib.NArith.BinNatDef.html @@ -61,7 +61,7 @@

Library Stdlib.NArith.BinNatDef

-

Binary natural numbers, definitions of operations

+

Binary natural numbers, definitions of operations

@@ -79,7 +79,7 @@

Library Stdlib.NArith.BinNatDef

-

Nicer name N.pos for constructor Npos

+

Nicer name N.pos for constructor Npos

@@ -91,7 +91,7 @@

Library Stdlib.NArith.BinNatDef

-

Constants

+

Constants

@@ -105,7 +105,7 @@

Library Stdlib.NArith.BinNatDef

-

Successor

+

Successor

@@ -121,7 +121,7 @@

Library Stdlib.NArith.BinNatDef

-

Predecessor

+

Predecessor

@@ -137,7 +137,7 @@

Library Stdlib.NArith.BinNatDef

-

Addition

+

Addition

diff --git a/v9.0/stdlib/Stdlib.NArith.Nnat.html b/v9.0/stdlib/Stdlib.NArith.Nnat.html index 7dbeb68563..22a7af4450 100644 --- a/v9.0/stdlib/Stdlib.NArith.Nnat.html +++ b/v9.0/stdlib/Stdlib.NArith.Nnat.html @@ -51,7 +51,7 @@

Library Stdlib.NArith.Nnat

-

Conversions from N to nat

+

Conversions from N to nat

@@ -167,7 +167,7 @@

Library Stdlib.NArith.Nnat

-

Conversions from nat to N

+

Conversions from nat to N

diff --git a/v9.0/stdlib/Stdlib.Numbers.AltBinNotations.html b/v9.0/stdlib/Stdlib.Numbers.AltBinNotations.html index 5c21c0237f..9fc08b8a2c 100644 --- a/v9.0/stdlib/Stdlib.Numbers.AltBinNotations.html +++ b/v9.0/stdlib/Stdlib.Numbers.AltBinNotations.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.AltBinNotations

-

Alternative Binary Number Notations

+

Alternative Binary Number Notations

diff --git a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms.html b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms.html index 3232e5a9f8..451f6317ab 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms.html +++ b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms

-

Signature and specification of bounded integers

+

Signature and specification of bounded integers

diff --git a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.NZCyclic.html b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.NZCyclic.html index 858be997df..57fc05f859 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.NZCyclic.html +++ b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Abstract.NZCyclic.html @@ -56,7 +56,7 @@

Library Stdlib.Numbers.Cyclic.Abstract.NZCyclic

-

From CyclicType to NZAxiomsSig

+

From CyclicType to NZAxiomsSig

diff --git a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Cyclic63.html b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Cyclic63.html index 1e54adef5f..b806c04fde 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Cyclic63.html +++ b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Cyclic63.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.Cyclic.Int63.Cyclic63

-

Uint63 numbers defines indeed a cyclic structure : Z/(2^63)Z

+

Uint63 numbers defines indeed a cyclic structure : Z/(2^63)Z

diff --git a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Ring63.html b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Ring63.html index 797b90c6b0..e8cc4e91d5 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Ring63.html +++ b/v9.0/stdlib/Stdlib.Numbers.Cyclic.Int63.Ring63.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.Cyclic.Int63.Ring63

-

Uint63 numbers defines Z/(2^63)Z, and can hence be equipped

+

Uint63 numbers defines Z/(2^63)Z, and can hence be equipped

with a ring structure and a ring tactic
diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalFacts.html b/v9.0/stdlib/Stdlib.Numbers.DecimalFacts.html index 86f27b3aec..94c3e455ef 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalFacts.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalFacts.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalFacts

-

DecimalFacts : some facts about Decimal numbers

+

DecimalFacts : some facts about Decimal numbers

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalN.html b/v9.0/stdlib/Stdlib.Numbers.DecimalN.html index 3acea63592..04b4ca8041 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalN.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalN.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalN

-

DecimalN

+

DecimalN

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalNat.html b/v9.0/stdlib/Stdlib.Numbers.DecimalNat.html index 163a37008f..9a913db6b8 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalNat.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalNat.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalNat

-

DecimalNat

+

DecimalNat

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalPos.html b/v9.0/stdlib/Stdlib.Numbers.DecimalPos.html index d79c25000d..bae2d449d6 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalPos.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalPos.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalPos

-

DecimalPos

+

DecimalPos

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalQ.html b/v9.0/stdlib/Stdlib.Numbers.DecimalQ.html index 01963a9950..be35b3a6bd 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalQ.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalQ.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalQ

-

DecimalQ

+

DecimalQ

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalR.html b/v9.0/stdlib/Stdlib.Numbers.DecimalR.html index 59824e94e5..cfd578c24c 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalR.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalR.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalR

-

DecimalR

+

DecimalR

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalString.html b/v9.0/stdlib/Stdlib.Numbers.DecimalString.html index f23dea974e..644598b60d 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalString.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalString.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.DecimalString

-

Conversion between decimal numbers and Coq strings

+

Conversion between decimal numbers and Coq strings

diff --git a/v9.0/stdlib/Stdlib.Numbers.DecimalZ.html b/v9.0/stdlib/Stdlib.Numbers.DecimalZ.html index fd62b7c4f0..0db078e010 100644 --- a/v9.0/stdlib/Stdlib.Numbers.DecimalZ.html +++ b/v9.0/stdlib/Stdlib.Numbers.DecimalZ.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.DecimalZ

-

DecimalZ

+

DecimalZ

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalFacts.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalFacts.html index 43fed7d6f2..4f0c66f08b 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalFacts.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalFacts.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalFacts

-

HexadecimalFacts : some facts about Hexadecimal numbers

+

HexadecimalFacts : some facts about Hexadecimal numbers

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalN.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalN.html index edf59dcbd5..0d43c77c30 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalN.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalN.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalN

-

HexadecimalN

+

HexadecimalN

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalNat.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalNat.html index 845fa04551..946e7b29d8 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalNat.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalNat.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalNat

-

HexadecimalNat

+

HexadecimalNat

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalPos.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalPos.html index 81b44fe5a1..c5dce1dcff 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalPos.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalPos.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalPos

-

HexadecimalPos

+

HexadecimalPos

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalQ.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalQ.html index 78b8f917da..f08bc5d597 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalQ.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalQ.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalQ

-

HexadecimalQ

+

HexadecimalQ

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalR.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalR.html index 7adc86be53..a85e989173 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalR.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalR.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalR

-

HexadecimalR

+

HexadecimalR

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalString.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalString.html index 56b1821fa1..049cbf3328 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalString.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalString.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.HexadecimalString

-

Conversion between hexadecimal numbers and Coq strings

+

Conversion between hexadecimal numbers and Coq strings

diff --git a/v9.0/stdlib/Stdlib.Numbers.HexadecimalZ.html b/v9.0/stdlib/Stdlib.Numbers.HexadecimalZ.html index 77e00bf0a3..07c7bd7d6a 100644 --- a/v9.0/stdlib/Stdlib.Numbers.HexadecimalZ.html +++ b/v9.0/stdlib/Stdlib.Numbers.HexadecimalZ.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.HexadecimalZ

-

HexadecimalZ

+

HexadecimalZ

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZBits.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZBits.html index 76433745ad..b50bb22a25 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZBits.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZBits.html @@ -472,7 +472,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZBits

-

Properties of shifts

+

Properties of shifts

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivEucl.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivEucl.html index 7cd483f76a..d894886c5c 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivEucl.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivEucl.html @@ -54,7 +54,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivEucl

-

Euclidean Division for integers, Euclid convention

+

Euclidean Division for integers, Euclid convention

@@ -245,7 +245,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivEucl

-

Basic values of divisions and modulo.

+

Basic values of divisions and modulo.

@@ -281,7 +281,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivEucl

-

Order results about mod and div

+

Order results about mod and div

@@ -410,7 +410,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivEucl

-

Relations between usual operations and mod and div

+

Relations between usual operations and mod and div

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivFloor.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivFloor.html index 75944973db..e4ee711d00 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivFloor.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivFloor.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivFloor

-

Euclidean Division for integers (Floor convention)

+

Euclidean Division for integers (Floor convention)

@@ -283,7 +283,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivFloor

-

Basic values of divisions and modulo.

+

Basic values of divisions and modulo.

@@ -319,7 +319,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivFloor

-

Order results about mod and div

+

Order results about mod and div

@@ -456,7 +456,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivFloor

-

Relations between usual operations and mod and div

+

Relations between usual operations and mod and div

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivTrunc.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivTrunc.html index 7880513fb5..3b77137b0f 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivTrunc.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZDivTrunc.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivTrunc

-

Euclidean Division for integers (Trunc convention)

+

Euclidean Division for integers (Trunc convention)

@@ -208,7 +208,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivTrunc

-

Basic values of divisions and modulo.

+

Basic values of divisions and modulo.

@@ -306,7 +306,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivTrunc

-

Order results about rem and quot

+

Order results about rem and quot

@@ -441,7 +441,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZDivTrunc

-

Relations between usual operations and rem and quot

+

Relations between usual operations and rem and quot

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZLcm.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZLcm.html index 57594eed26..1389e2ef3c 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZLcm.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZLcm.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZLcm

-

Least Common Multiple

+

Least Common Multiple

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZMaxMin.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZMaxMin.html index ffc6fc6c0a..f70c7d73b9 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZMaxMin.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Abstract.ZMaxMin.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.Integer.Abstract.ZMaxMin

-

Properties of minimum and maximum specific to integer numbers

+

Properties of minimum and maximum specific to integer numbers

diff --git a/v9.0/stdlib/Stdlib.Numbers.Integer.Binary.ZBinary.html b/v9.0/stdlib/Stdlib.Numbers.Integer.Binary.ZBinary.html index 9131feb6cc..56a56db8f2 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Integer.Binary.ZBinary.html +++ b/v9.0/stdlib/Stdlib.Numbers.Integer.Binary.ZBinary.html @@ -70,7 +70,7 @@

Library Stdlib.Numbers.Integer.Binary.ZBinary

-

An order tactic for integers

+

An order tactic for integers

diff --git a/v9.0/stdlib/Stdlib.Numbers.NaryFunctions.html b/v9.0/stdlib/Stdlib.Numbers.NaryFunctions.html index 04a41fe753..432b94da12 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NaryFunctions.html +++ b/v9.0/stdlib/Stdlib.Numbers.NaryFunctions.html @@ -56,7 +56,7 @@

Library Stdlib.Numbers.NaryFunctions

-

Generic dependently-typed operators about n-ary functions

+

Generic dependently-typed operators about n-ary functions

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAdd.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAdd.html index 117e4df7f3..f41f5f630d 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAdd.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAdd.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.NatInt.NZAdd

-

Some properties of the addition for modules implementing NZBasicFunsSig'

+

Some properties of the addition for modules implementing NZBasicFunsSig'

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAddOrder.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAddOrder.html index 7de4bee2e1..8a0c12e0bc 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAddOrder.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAddOrder.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.NatInt.NZAddOrder

-

Properties of orders and addition for modules implementing NZOrdAxiomsSig'

+

Properties of orders and addition for modules implementing NZOrdAxiomsSig'

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAxioms.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAxioms.html index 47e0279a93..03132f7bb8 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAxioms.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZAxioms.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.NatInt.NZAxioms

Initial Author : Evgeny Makarov, INRIA, 2007
-

Axioms for a domain with zero, succ, pred.

+

Axioms for a domain with zero, succ, pred.

@@ -144,7 +144,7 @@

Library Stdlib.Numbers.NatInt.NZAxioms

-

Axiomatization of a domain with zero, succ, pred and a bi-directional induction principle.

+

Axiomatization of a domain with zero, succ, pred and a bi-directional induction principle.

@@ -226,7 +226,7 @@

Library Stdlib.Numbers.NatInt.NZAxioms

-

Axiomatization of some more constants

+

Axiomatization of some more constants

@@ -283,7 +283,7 @@

Library Stdlib.Numbers.NatInt.NZAxioms

-

Axiomatization of basic operations : + - *

+

Axiomatization of basic operations : + - *

@@ -339,7 +339,7 @@

Library Stdlib.Numbers.NatInt.NZAxioms

-

Axiomatization of order

+

Axiomatization of order

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZBase.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZBase.html index 684dcf3672..4f5c1163e2 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZBase.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZBase.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.NatInt.NZBase

-

Basic lemmas about modules implementing NZDomainSig'

+

Basic lemmas about modules implementing NZDomainSig'

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDiv.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDiv.html index a673067de6..39e3440ddf 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDiv.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDiv.html @@ -189,7 +189,7 @@

Library Stdlib.Numbers.NatInt.NZDiv

-

Basic values of divisions and modulo.

+

Basic values of divisions and modulo.

@@ -222,7 +222,7 @@

Library Stdlib.Numbers.NatInt.NZDiv

-

Order results about mod and div

+

Order results about mod and div

@@ -334,7 +334,7 @@

Library Stdlib.Numbers.NatInt.NZDiv

-

Relations between usual operations and mod and div

+

Relations between usual operations and mod and div

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDomain.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDomain.html index 372fe26802..5badcb1cd7 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDomain.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZDomain.html @@ -77,7 +77,7 @@

Library Stdlib.Numbers.NatInt.NZDomain

-

Relationship between points thanks to succ and pred.

+

Relationship between points thanks to succ and pred.

@@ -128,7 +128,7 @@

Library Stdlib.Numbers.NatInt.NZDomain

-

Study of initial point w.r.t. succ (if any).

+

Study of initial point w.r.t. succ (if any).

@@ -252,7 +252,7 @@

Library Stdlib.Numbers.NatInt.NZDomain

-

An alternative induction principle using S and P.

+

An alternative induction principle using S and P.

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZLog.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZLog.html index aeb7845680..a0a97fae81 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZLog.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZLog.html @@ -417,7 +417,7 @@

Library Stdlib.Numbers.NatInt.NZLog

-

log2_up : a binary logarithm that rounds up instead of down

+

log2_up : a binary logarithm that rounds up instead of down

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMul.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMul.html index 1e1075da5d..d4e04a9d16 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMul.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMul.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.NatInt.NZMul

-

Some properties of the multiplication for modules implementing NZBasicFunsSig'

+

Some properties of the multiplication for modules implementing NZBasicFunsSig'

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMulOrder.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMulOrder.html index 7daa764b58..012d60671e 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMulOrder.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZMulOrder.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.NatInt.NZMulOrder

-

Properties of orders and multiplication for modules implementing NZOrdAxiomsSig'

+

Properties of orders and multiplication for modules implementing NZOrdAxiomsSig'

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZOrder.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZOrder.html index 47a541b061..cafdabeb4a 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZOrder.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZOrder.html @@ -48,7 +48,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Lemmas about orders for modules implementing NZOrdSig'

+

Lemmas about orders for modules implementing NZOrdSig'

@@ -104,11 +104,11 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Basic facts about le, lt, eq and succ

+

Basic facts about le, lt, eq and succ

-

Direct consequences of the specifications of lt and le

+

Direct consequences of the specifications of lt and le

@@ -166,7 +166,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Asymmetry and transitivity.

+

Asymmetry and transitivity.

@@ -187,7 +187,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Some type classes about order

+

Some type classes about order

@@ -208,7 +208,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Making the generic order tactic

+

Making the generic order tactic

@@ -235,7 +235,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Some direct consequences of order

+

Some direct consequences of order

@@ -280,7 +280,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

More properties of < and <= with respect to S and 0

+

More properties of < and <= with respect to S and 0

@@ -336,7 +336,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

More Trichotomy, decidability and double negation elimination

+

More Trichotomy, decidability and double negation elimination

@@ -447,7 +447,7 @@

Library Stdlib.Numbers.NatInt.NZOrder

-

Order-based induction principles

+

Order-based induction principles

diff --git a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZSqrt.html b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZSqrt.html index b43cae94a5..e97022ee84 100644 --- a/v9.0/stdlib/Stdlib.Numbers.NatInt.NZSqrt.html +++ b/v9.0/stdlib/Stdlib.Numbers.NatInt.NZSqrt.html @@ -347,7 +347,7 @@

Library Stdlib.Numbers.NatInt.NZSqrt

-

sqrt_up : a square root that rounds up instead of down

+

sqrt_up : a square root that rounds up instead of down

diff --git a/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NDiv.html b/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NDiv.html index bbe970bebc..96c5826a2b 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NDiv.html +++ b/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NDiv.html @@ -157,7 +157,7 @@

Library Stdlib.Numbers.Natural.Abstract.NDiv

-

Basic values of divisions and modulo.

+

Basic values of divisions and modulo.

@@ -190,7 +190,7 @@

Library Stdlib.Numbers.Natural.Abstract.NDiv

-

Order results about mod and div

+

Order results about mod and div

@@ -288,7 +288,7 @@

Library Stdlib.Numbers.Natural.Abstract.NDiv

-

Relations between usual operations and mod and div

+

Relations between usual operations and mod and div

diff --git a/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NLcm.html b/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NLcm.html index 9f73ddf488..5d9101b237 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NLcm.html +++ b/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NLcm.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.Natural.Abstract.NLcm

-

Least Common Multiple

+

Least Common Multiple

diff --git a/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NMaxMin.html b/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NMaxMin.html index 17c6760f9f..701b191a3c 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NMaxMin.html +++ b/v9.0/stdlib/Stdlib.Numbers.Natural.Abstract.NMaxMin.html @@ -51,7 +51,7 @@

Library Stdlib.Numbers.Natural.Abstract.NMaxMin

-

Properties of minimum and maximum specific to natural numbers

+

Properties of minimum and maximum specific to natural numbers

diff --git a/v9.0/stdlib/Stdlib.Numbers.Natural.Binary.NBinary.html b/v9.0/stdlib/Stdlib.Numbers.Natural.Binary.NBinary.html index 32f800297c..ba8a3ca7d5 100644 --- a/v9.0/stdlib/Stdlib.Numbers.Natural.Binary.NBinary.html +++ b/v9.0/stdlib/Stdlib.Numbers.Natural.Binary.NBinary.html @@ -58,7 +58,7 @@

Library Stdlib.Numbers.Natural.Binary.NBinary

-

BinNat.N already implements NAxiomSig

+

BinNat.N already implements NAxiomSig

diff --git a/v9.0/stdlib/Stdlib.PArith.BinPos.html b/v9.0/stdlib/Stdlib.PArith.BinPos.html index f3e304fcc8..0fd40dbcf9 100644 --- a/v9.0/stdlib/Stdlib.PArith.BinPos.html +++ b/v9.0/stdlib/Stdlib.PArith.BinPos.html @@ -56,7 +56,7 @@

Library Stdlib.PArith.BinPos

-

Binary positive numbers, operations and properties

+

Binary positive numbers, operations and properties

@@ -90,7 +90,7 @@

Library Stdlib.PArith.BinPos

-

Definitions of operations, now in a separate file

+

Definitions of operations, now in a separate file

@@ -112,7 +112,7 @@

Library Stdlib.PArith.BinPos

-

Logical Predicates

+

Logical Predicates

@@ -144,11 +144,11 @@

Library Stdlib.PArith.BinPos

-

Properties of operations over positive numbers

+

Properties of operations over positive numbers

-

Decidability of equality on binary positive numbers

+

Decidability of equality on binary positive numbers

@@ -160,11 +160,11 @@

Library Stdlib.PArith.BinPos

-

Properties of successor on binary positive numbers

+

Properties of successor on binary positive numbers

-

Specification of xI in term of succ and xO

+

Specification of xI in term of succ and xO

@@ -179,7 +179,7 @@

Library Stdlib.PArith.BinPos

-

Successor and double

+

Successor and double

@@ -203,7 +203,7 @@

Library Stdlib.PArith.BinPos

-

Successor and predecessor

+

Successor and predecessor

@@ -224,7 +224,7 @@

Library Stdlib.PArith.BinPos

-

Injectivity of successor

+

Injectivity of successor

@@ -236,7 +236,7 @@

Library Stdlib.PArith.BinPos

-

Predecessor to N

+

Predecessor to N

@@ -248,11 +248,11 @@

Library Stdlib.PArith.BinPos

-

Properties of addition on binary positive numbers

+

Properties of addition on binary positive numbers

-

Specification of succ in term of add

+

Specification of succ in term of add

@@ -267,7 +267,7 @@

Library Stdlib.PArith.BinPos

-

Specification of add_carry

+

Specification of add_carry

@@ -279,7 +279,7 @@

Library Stdlib.PArith.BinPos

-

Commutativity

+

Commutativity

@@ -291,7 +291,7 @@

Library Stdlib.PArith.BinPos

-

Permutation of add and succ

+

Permutation of add and succ

@@ -306,7 +306,7 @@

Library Stdlib.PArith.BinPos

-

No neutral elements for addition

+

No neutral elements for addition

@@ -316,7 +316,7 @@

Library Stdlib.PArith.BinPos

-

Simplification

+

Simplification

@@ -349,7 +349,7 @@

Library Stdlib.PArith.BinPos

-

Addition is associative

+

Addition is associative

@@ -361,7 +361,7 @@

Library Stdlib.PArith.BinPos

-

Commutation of addition and double

+

Commutation of addition and double

@@ -381,7 +381,7 @@

Library Stdlib.PArith.BinPos

-

Miscellaneous

+

Miscellaneous

@@ -393,7 +393,7 @@

Library Stdlib.PArith.BinPos

-

Peano induction and recursion on binary positive positive numbers

+

Peano induction and recursion on binary positive positive numbers

@@ -511,11 +511,11 @@

Library Stdlib.PArith.BinPos

-

Properties of multiplication on binary positive numbers

+

Properties of multiplication on binary positive numbers

-

One is neutral for multiplication

+

One is neutral for multiplication

@@ -530,7 +530,7 @@

Library Stdlib.PArith.BinPos

-

Right reduction properties for multiplication

+

Right reduction properties for multiplication

@@ -545,7 +545,7 @@

Library Stdlib.PArith.BinPos

-

Commutativity of multiplication

+

Commutativity of multiplication

@@ -557,7 +557,7 @@

Library Stdlib.PArith.BinPos

-

Distributivity of multiplication over addition

+

Distributivity of multiplication over addition

@@ -574,7 +574,7 @@

Library Stdlib.PArith.BinPos

-

Associativity of multiplication

+

Associativity of multiplication

@@ -586,7 +586,7 @@

Library Stdlib.PArith.BinPos

-

Successor and multiplication

+

Successor and multiplication

@@ -601,7 +601,7 @@

Library Stdlib.PArith.BinPos

-

Parity properties of multiplication

+

Parity properties of multiplication

@@ -616,7 +616,7 @@

Library Stdlib.PArith.BinPos

-

Simplification properties of multiplication

+

Simplification properties of multiplication

@@ -637,7 +637,7 @@

Library Stdlib.PArith.BinPos

-

Inversion of multiplication

+

Inversion of multiplication

@@ -655,7 +655,7 @@

Library Stdlib.PArith.BinPos

-

Square

+

Square

@@ -670,7 +670,7 @@

Library Stdlib.PArith.BinPos

-

Properties of iter

+

Properties of iter

@@ -716,7 +716,7 @@

Library Stdlib.PArith.BinPos

-

Properties of power

+

Properties of power

@@ -731,7 +731,7 @@

Library Stdlib.PArith.BinPos

-

Properties of square

+

Properties of square

@@ -743,7 +743,7 @@

Library Stdlib.PArith.BinPos

-

Properties of sub_mask

+

Properties of sub_mask

@@ -790,7 +790,7 @@

Library Stdlib.PArith.BinPos

-

Properties of boolean comparisons

+

Properties of boolean comparisons

@@ -819,7 +819,7 @@

Library Stdlib.PArith.BinPos

-

Properties of comparison on binary positive numbers

+

Properties of comparison on binary positive numbers

@@ -1013,7 +1013,7 @@

Library Stdlib.PArith.BinPos

-

Facts about gt and ge

+

Facts about gt and ge

@@ -1046,7 +1046,7 @@

Library Stdlib.PArith.BinPos

-

Comparison and the successor

+

Comparison and the successor

@@ -1072,7 +1072,7 @@

Library Stdlib.PArith.BinPos

-

1 is the least positive number

+

1 is the least positive number

@@ -1090,7 +1090,7 @@

Library Stdlib.PArith.BinPos

-

Properties of the order

+

Properties of the order

@@ -1163,7 +1163,7 @@

Library Stdlib.PArith.BinPos

-

Comparison and addition

+

Comparison and addition

@@ -1178,7 +1178,7 @@

Library Stdlib.PArith.BinPos

-

Order and addition

+

Order and addition

@@ -1208,7 +1208,7 @@

Library Stdlib.PArith.BinPos

-

Comparison and multiplication

+

Comparison and multiplication

@@ -1223,7 +1223,7 @@

Library Stdlib.PArith.BinPos

-

Order and multiplication

+

Order and multiplication

@@ -1259,7 +1259,7 @@

Library Stdlib.PArith.BinPos

-

Properties of subtraction on binary positive numbers

+

Properties of subtraction on binary positive numbers

@@ -1277,7 +1277,7 @@

Library Stdlib.PArith.BinPos

-

Properties of subtraction without underflow

+

Properties of subtraction without underflow

@@ -1375,7 +1375,7 @@

Library Stdlib.PArith.BinPos

-

Results concerning size and size_nat

+

Results concerning size and size_nat

@@ -1393,7 +1393,7 @@

Library Stdlib.PArith.BinPos

-

Properties of min and max

+

Properties of min and max

@@ -1489,7 +1489,7 @@

Library Stdlib.PArith.BinPos

-

Results concerning iter_op

+

Results concerning iter_op

@@ -1510,7 +1510,7 @@

Library Stdlib.PArith.BinPos

-

Results about of_nat and of_succ_nat

+

Results about of_nat and of_succ_nat

@@ -1528,7 +1528,7 @@

Library Stdlib.PArith.BinPos

-

Correctness proofs for the square root function

+

Correctness proofs for the square root function

@@ -1554,7 +1554,7 @@

Library Stdlib.PArith.BinPos

-

Correctness proofs for the gcd function

+

Correctness proofs for the gcd function

diff --git a/v9.0/stdlib/Stdlib.PArith.BinPosDef.html b/v9.0/stdlib/Stdlib.PArith.BinPosDef.html index c276fad83c..b9b689e1bc 100644 --- a/v9.0/stdlib/Stdlib.PArith.BinPosDef.html +++ b/v9.0/stdlib/Stdlib.PArith.BinPosDef.html @@ -48,7 +48,7 @@

Library Stdlib.PArith.BinPosDef

-

Binary positive numbers, operations

+

Binary positive numbers, operations

@@ -79,7 +79,7 @@

Library Stdlib.PArith.BinPosDef

-

Operations over positive numbers

+

Operations over positive numbers

@@ -91,7 +91,7 @@

Library Stdlib.PArith.BinPosDef

-

Predecessor

+

Predecessor

@@ -108,7 +108,7 @@

Library Stdlib.PArith.BinPosDef

-

Predecessor with mask

+

Predecessor with mask

@@ -132,7 +132,7 @@

Library Stdlib.PArith.BinPosDef

-

Power

+

Power

@@ -147,7 +147,7 @@

Library Stdlib.PArith.BinPosDef

-

Square

+

Square

@@ -164,7 +164,7 @@

Library Stdlib.PArith.BinPosDef

-

Number of digits in a positive number

+

Number of digits in a positive number

@@ -214,7 +214,7 @@

Library Stdlib.PArith.BinPosDef

-

Boolean equality and comparisons

+

Boolean equality and comparisons

@@ -232,7 +232,7 @@

Library Stdlib.PArith.BinPosDef

-

Greatest Common Divisor

+

Greatest Common Divisor

@@ -397,7 +397,7 @@

Library Stdlib.PArith.BinPosDef

-

From Peano natural numbers to binary positive numbers

+

From Peano natural numbers to binary positive numbers

@@ -417,7 +417,7 @@

Library Stdlib.PArith.BinPosDef

-

Conversion with a decimal representation for printing/parsing

+

Conversion with a decimal representation for printing/parsing

diff --git a/v9.0/stdlib/Stdlib.PArith.POrderedType.html b/v9.0/stdlib/Stdlib.PArith.POrderedType.html index 3657a2d94e..1266851bcb 100644 --- a/v9.0/stdlib/Stdlib.PArith.POrderedType.html +++ b/v9.0/stdlib/Stdlib.PArith.POrderedType.html @@ -54,7 +54,7 @@

Library Stdlib.PArith.POrderedType

-

DecidableType structure for positive numbers

+

DecidableType structure for positive numbers

@@ -70,7 +70,7 @@

Library Stdlib.PArith.POrderedType

interfaces, such as DecidableType or EqualityType.
-

OrderedType structure for positive numbers

+

OrderedType structure for positive numbers

@@ -86,7 +86,7 @@

Library Stdlib.PArith.POrderedType

and a OrderedType (and also as a DecidableType).
-

An order tactic for positive numbers

+

An order tactic for positive numbers

diff --git a/v9.0/stdlib/Stdlib.Program.Combinators.html b/v9.0/stdlib/Stdlib.Program.Combinators.html index 9e93dd2ed6..e4b8bc1dbf 100644 --- a/v9.0/stdlib/Stdlib.Program.Combinators.html +++ b/v9.0/stdlib/Stdlib.Program.Combinators.html @@ -46,7 +46,7 @@

Library Stdlib.Program.Combinators

-

Proofs about standard combinators, exports functional extensionality.

+

Proofs about standard combinators, exports functional extensionality.

diff --git a/v9.0/stdlib/Stdlib.QArith.QArith_base.html b/v9.0/stdlib/Stdlib.QArith.QArith_base.html index 601fbe618e..d030421750 100644 --- a/v9.0/stdlib/Stdlib.QArith.QArith_base.html +++ b/v9.0/stdlib/Stdlib.QArith.QArith_base.html @@ -58,7 +58,7 @@

Library Stdlib.QArith.QArith_base

-

Definition of Q and basic properties

+

Definition of Q and basic properties

@@ -201,7 +201,7 @@

Library Stdlib.QArith.QArith_base

-

Properties of equality.

+

Properties of equality.

@@ -293,7 +293,7 @@

Library Stdlib.QArith.QArith_base

-

Addition, multiplication and opposite

+

Addition, multiplication and opposite

@@ -560,7 +560,7 @@

Library Stdlib.QArith.QArith_base

-

Setoid compatibility results

+

Setoid compatibility results

@@ -634,7 +634,7 @@

Library Stdlib.QArith.QArith_base

-

Properties of Qadd

+

Properties of Qadd

@@ -674,7 +674,7 @@

Library Stdlib.QArith.QArith_base

-

Properties of Qopp

+

Properties of Qopp

@@ -705,7 +705,7 @@

Library Stdlib.QArith.QArith_base

-

Properties of Qmult

+

Properties of Qmult

@@ -787,7 +787,7 @@

Library Stdlib.QArith.QArith_base

-

inject_Z is a ring homomorphism:

+

inject_Z is a ring homomorphism:

@@ -805,7 +805,7 @@

Library Stdlib.QArith.QArith_base

-

Inverse and division.

+

Inverse and division.

@@ -857,11 +857,11 @@

Library Stdlib.QArith.QArith_base

-

Reduction and construction of Q

+

Reduction and construction of Q

-

Removal/introduction of common factor in both numerator and denominator.

+

Removal/introduction of common factor in both numerator and denominator.

@@ -906,7 +906,7 @@

Library Stdlib.QArith.QArith_base

-

Construction of a new rational by multiplication with an integer or pure fraction

+

Construction of a new rational by multiplication with an integer or pure fraction

@@ -932,7 +932,7 @@

Library Stdlib.QArith.QArith_base

-

Properties of order upon Q.

+

Properties of order upon Q.

@@ -1046,7 +1046,7 @@

Library Stdlib.QArith.QArith_base

-

Some decidability results about orders.

+

Some decidability results about orders.

@@ -1064,7 +1064,7 @@

Library Stdlib.QArith.QArith_base

-

Compatibility of addition with order

+

Compatibility of addition with order

@@ -1117,7 +1117,7 @@

Library Stdlib.QArith.QArith_base

-

Compatibility of multiplication with order.

+

Compatibility of multiplication with order.

@@ -1176,7 +1176,7 @@

Library Stdlib.QArith.QArith_base

-

Compatibility of inversion and division with order

+

Compatibility of inversion and division with order

@@ -1227,7 +1227,7 @@

Library Stdlib.QArith.QArith_base

-

Rational to the n-th power

+

Rational to the n-th power

diff --git a/v9.0/stdlib/Stdlib.QArith.QOrderedType.html b/v9.0/stdlib/Stdlib.QArith.QOrderedType.html index 4728166d04..81f55fd3b4 100644 --- a/v9.0/stdlib/Stdlib.QArith.QOrderedType.html +++ b/v9.0/stdlib/Stdlib.QArith.QOrderedType.html @@ -54,7 +54,7 @@

Library Stdlib.QArith.QOrderedType

-

DecidableType structure for rational numbers

+

DecidableType structure for rational numbers

@@ -92,7 +92,7 @@

Library Stdlib.QArith.QOrderedType

interfaces, such as DecidableType or EqualityType.
-

OrderedType structure for rational numbers

+

OrderedType structure for rational numbers

@@ -123,7 +123,7 @@

Library Stdlib.QArith.QOrderedType

-

An order tactic for Q numbers

+

An order tactic for Q numbers

diff --git a/v9.0/stdlib/Stdlib.QArith.Qcabs.html b/v9.0/stdlib/Stdlib.QArith.Qcabs.html index ae2200e425..0b3cfebf91 100644 --- a/v9.0/stdlib/Stdlib.QArith.Qcabs.html +++ b/v9.0/stdlib/Stdlib.QArith.Qcabs.html @@ -48,7 +48,7 @@

Library Stdlib.QArith.Qcabs

-

An absolute value for normalized rational numbers.

+

An absolute value for normalized rational numbers.

diff --git a/v9.0/stdlib/Stdlib.QArith.Qfield.html b/v9.0/stdlib/Stdlib.QArith.Qfield.html index 71a5adae0a..05c5c075d0 100644 --- a/v9.0/stdlib/Stdlib.QArith.Qfield.html +++ b/v9.0/stdlib/Stdlib.QArith.Qfield.html @@ -53,7 +53,7 @@

Library Stdlib.QArith.Qfield

-

field and ring tactics for rational numbers

+

field and ring tactics for rational numbers

diff --git a/v9.0/stdlib/Stdlib.QArith.Qminmax.html b/v9.0/stdlib/Stdlib.QArith.Qminmax.html index 1b39f9d14c..ed3e3cb6da 100644 --- a/v9.0/stdlib/Stdlib.QArith.Qminmax.html +++ b/v9.0/stdlib/Stdlib.QArith.Qminmax.html @@ -51,7 +51,7 @@

Library Stdlib.QArith.Qminmax

-

Maximum and Minimum of two rational numbers

+

Maximum and Minimum of two rational numbers

@@ -100,7 +100,7 @@

Library Stdlib.QArith.Qminmax

-

Properties specific to the Q domain

+

Properties specific to the Q domain

diff --git a/v9.0/stdlib/Stdlib.QArith.Qpower.html b/v9.0/stdlib/Stdlib.QArith.Qpower.html index 6a9d659398..d4b3883c9e 100644 --- a/v9.0/stdlib/Stdlib.QArith.Qpower.html +++ b/v9.0/stdlib/Stdlib.QArith.Qpower.html @@ -51,11 +51,11 @@

Library Stdlib.QArith.Qpower

-

Properties of Qpower_positive

+

Properties of Qpower_positive

-

Values of Qpower_positive for specific arguments

+

Values of Qpower_positive for specific arguments

@@ -70,7 +70,7 @@

Library Stdlib.QArith.Qpower

-

Relation of Qpower_positive to zero

+

Relation of Qpower_positive to zero

@@ -85,7 +85,7 @@

Library Stdlib.QArith.Qpower

-

Qpower_positive and multiplication, exponent subtraction

+

Qpower_positive and multiplication, exponent subtraction

@@ -100,7 +100,7 @@

Library Stdlib.QArith.Qpower

-

Qpower_positive and inversion, division, exponent subtraction

+

Qpower_positive and inversion, division, exponent subtraction

@@ -117,7 +117,7 @@

Library Stdlib.QArith.Qpower

-

Qpower and exponent multiplication

+

Qpower and exponent multiplication

@@ -130,7 +130,7 @@

Library Stdlib.QArith.Qpower

-

Qpower_positive decomposition

+

Qpower_positive decomposition

@@ -146,11 +146,11 @@

Library Stdlib.QArith.Qpower

-

Properties of Qpower

+

Properties of Qpower

-

Values of Qpower for specific arguments

+

Values of Qpower for specific arguments

@@ -173,7 +173,7 @@

Library Stdlib.QArith.Qpower

-

Relation of Qpower to zero

+

Relation of Qpower to zero

@@ -195,7 +195,7 @@

Library Stdlib.QArith.Qpower

-

Relation of Qpower to 1

+

Relation of Qpower to 1

@@ -220,7 +220,7 @@

Library Stdlib.QArith.Qpower

-

Qpower and multiplication, exponent addition

+

Qpower and multiplication, exponent addition

@@ -238,7 +238,7 @@

Library Stdlib.QArith.Qpower

-

Qpower and inversion, division, exponent subtraction

+

Qpower and inversion, division, exponent subtraction

@@ -271,7 +271,7 @@

Library Stdlib.QArith.Qpower

-

Qpower and exponent multiplication

+

Qpower and exponent multiplication

@@ -283,7 +283,7 @@

Library Stdlib.QArith.Qpower

-

Qpower decomposition

+

Qpower decomposition

@@ -304,7 +304,7 @@

Library Stdlib.QArith.Qpower

-

Compatibility of Qpower with relational operators

+

Compatibility of Qpower with relational operators

@@ -329,7 +329,7 @@

Library Stdlib.QArith.Qpower

-

Qpower and inject_Z

+

Qpower and inject_Z

@@ -341,7 +341,7 @@

Library Stdlib.QArith.Qpower

-

Square

+

Square

@@ -353,7 +353,7 @@

Library Stdlib.QArith.Qpower

-

Power of 2 positive upper bound

+

Power of 2 positive upper bound

diff --git a/v9.0/stdlib/Stdlib.Reals.AltSeries.html b/v9.0/stdlib/Stdlib.Reals.AltSeries.html index ee287ce0c9..3049e3cbb2 100644 --- a/v9.0/stdlib/Stdlib.Reals.AltSeries.html +++ b/v9.0/stdlib/Stdlib.Reals.AltSeries.html @@ -58,7 +58,7 @@

Library Stdlib.Reals.AltSeries

-

Formalization of alternated series

+

Formalization of alternated series

@@ -121,7 +121,7 @@

Library Stdlib.Reals.AltSeries

-

Convergence of alternated series

+

Convergence of alternated series

@@ -143,7 +143,7 @@

Library Stdlib.Reals.AltSeries

-

Application : construction of PI

+

Application : construction of PI

diff --git a/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyReals.html b/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyReals.html index 1caf185a4e..9206c5b7d0 100644 --- a/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyReals.html +++ b/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyReals.html @@ -407,7 +407,7 @@

Library Stdlib.Reals.Cauchy.ConstructiveCauchyReals

-

Algebraic operations

+

Algebraic operations

diff --git a/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult.html b/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult.html index 1b13f3b72e..195321bc13 100644 --- a/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult.html +++ b/v9.0/stdlib/Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult.html @@ -297,7 +297,7 @@

Library Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult

-

Field

+

Field

diff --git a/v9.0/stdlib/Stdlib.Reals.Cauchy.QExtra.html b/v9.0/stdlib/Stdlib.Reals.Cauchy.QExtra.html index 7eb3ed4946..b58d8e0136 100644 --- a/v9.0/stdlib/Stdlib.Reals.Cauchy.QExtra.html +++ b/v9.0/stdlib/Stdlib.Reals.Cauchy.QExtra.html @@ -55,7 +55,7 @@

Library Stdlib.Reals.Cauchy.QExtra

-

Power of 2 open and closed upper and lower bounds for q : Q

+

Power of 2 open and closed upper and lower bounds for q : Q

@@ -96,7 +96,7 @@

Library Stdlib.Reals.Cauchy.QExtra

-

Power of two closed upper bound q <= 2^z

+

Power of two closed upper bound q <= 2^z

@@ -125,7 +125,7 @@

Library Stdlib.Reals.Cauchy.QExtra

-

Power of two open upper bound q < 2^z and Qabs q < 2^z

+

Power of two open upper bound q < 2^z and Qabs q < 2^z

@@ -171,7 +171,7 @@

Library Stdlib.Reals.Cauchy.QExtra

-

Power of 2 open lower bounds for 2^z < q and 2^z < Qabs q

+

Power of 2 open lower bounds for 2^z < q and 2^z < Qabs q

@@ -202,7 +202,7 @@

Library Stdlib.Reals.Cauchy.QExtra

-

Existential formulations of power of 2 lower and upper bounds

+

Existential formulations of power of 2 lower and upper bounds

diff --git a/v9.0/stdlib/Stdlib.Reals.ClassicalDedekindReals.html b/v9.0/stdlib/Stdlib.Reals.ClassicalDedekindReals.html index 6ea22f72c3..1b101e3c42 100644 --- a/v9.0/stdlib/Stdlib.Reals.ClassicalDedekindReals.html +++ b/v9.0/stdlib/Stdlib.Reals.ClassicalDedekindReals.html @@ -64,7 +64,7 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Q Auxiliary Lemmas

+

Q Auxiliary Lemmas

@@ -87,11 +87,11 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Dedekind cuts

+

Dedekind cuts

-

Definition

+

Definition

@@ -133,7 +133,7 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Properties

+

Properties

@@ -165,11 +165,11 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Classical Dedekind reals

+

Classical Dedekind reals

-

Definition

+

Definition

@@ -182,7 +182,7 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Induction principle

+

Induction principle

@@ -196,11 +196,11 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Conversion to and from constructive Cauchy real CReal

+

Conversion to and from constructive Cauchy real CReal

-

Conversion from CReal to DReal

+

Conversion from CReal to DReal

@@ -219,7 +219,7 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Conversion from DReal to CReal

+

Conversion from DReal to CReal

@@ -270,7 +270,7 @@

Library Stdlib.Reals.ClassicalDedekindReals

-

Order for DReal

+

Order for DReal

diff --git a/v9.0/stdlib/Stdlib.Reals.RIneq.html b/v9.0/stdlib/Stdlib.Reals.RIneq.html index 572b083825..0f000251f8 100644 --- a/v9.0/stdlib/Stdlib.Reals.RIneq.html +++ b/v9.0/stdlib/Stdlib.Reals.RIneq.html @@ -48,7 +48,7 @@

Library Stdlib.Reals.RIneq

-

Basic lemmas for the classical real numbers

+

Basic lemmas for the classical real numbers

@@ -136,7 +136,7 @@

Library Stdlib.Reals.RIneq

-

Relation between orders and equality

+

Relation between orders and equality

@@ -226,7 +226,7 @@

Library Stdlib.Reals.RIneq

-

Strong decidable equality

+

Strong decidable equality

@@ -238,11 +238,11 @@

Library Stdlib.Reals.RIneq

-

Relating <, >, <= and >=

+

Relating <, >, <= and >=

-

Relating strict and large orders

+

Relating strict and large orders

@@ -347,7 +347,7 @@

Library Stdlib.Reals.RIneq

-

Asymmetry

+

Asymmetry

@@ -368,7 +368,7 @@

Library Stdlib.Reals.RIneq

-

Antisymmetry

+

Antisymmetry

@@ -397,7 +397,7 @@

Library Stdlib.Reals.RIneq

-

Compatibility with equality

+

Compatibility with equality

@@ -414,7 +414,7 @@

Library Stdlib.Reals.RIneq

-

Transitivity

+

Transitivity

@@ -457,7 +457,7 @@

Library Stdlib.Reals.RIneq

-

(Classical) decidability with sumbool types

+

(Classical) decidability with sumbool types

@@ -508,7 +508,7 @@

Library Stdlib.Reals.RIneq

-

Same theorems with disjunctions instead of sumbools

+

Same theorems with disjunctions instead of sumbools

@@ -562,7 +562,7 @@

Library Stdlib.Reals.RIneq

-

Addition

+

Addition

@@ -636,7 +636,7 @@

Library Stdlib.Reals.RIneq

-

Opposite

+

Opposite

@@ -678,7 +678,7 @@

Library Stdlib.Reals.RIneq

-

Multiplication

+

Multiplication

@@ -794,7 +794,7 @@

Library Stdlib.Reals.RIneq

-

Opposite and multiplication

+

Opposite and multiplication

@@ -822,7 +822,7 @@

Library Stdlib.Reals.RIneq

-

Subtraction

+

Subtraction

@@ -934,7 +934,7 @@

Library Stdlib.Reals.RIneq

-

Inverse

+

Inverse

@@ -988,7 +988,7 @@

Library Stdlib.Reals.RIneq

-

Square function

+

Square function

@@ -1010,11 +1010,11 @@

Library Stdlib.Reals.RIneq

-

Order and addition

+

Order and addition

-

Compatibility

+

Compatibility

@@ -1115,7 +1115,7 @@

Library Stdlib.Reals.RIneq

-

Cancellation

+

Cancellation

@@ -1167,7 +1167,7 @@

Library Stdlib.Reals.RIneq

-

Comparison of addition with left operand

+

Comparison of addition with left operand

@@ -1188,7 +1188,7 @@

Library Stdlib.Reals.RIneq

-

Sign of addition

+

Sign of addition

@@ -1221,11 +1221,11 @@

Library Stdlib.Reals.RIneq

-

Order and opposite

+

Order and opposite

-

Contravariant compatibility

+

Contravariant compatibility

@@ -1301,7 +1301,7 @@

Library Stdlib.Reals.RIneq

-

Cancellation

+

Cancellation

@@ -1326,7 +1326,7 @@

Library Stdlib.Reals.RIneq

-

Sign of opposite

+

Sign of opposite

@@ -1341,14 +1341,14 @@

Library Stdlib.Reals.RIneq

-

Order and multiplication

+

Order and multiplication

Remark: Rmult_lt_compat_l is in Raxioms.v
-

Covariant compatibility

+

Covariant compatibility

@@ -1419,7 +1419,7 @@

Library Stdlib.Reals.RIneq

-

Contravariant compatibility

+

Contravariant compatibility

@@ -1444,7 +1444,7 @@

Library Stdlib.Reals.RIneq

-

Sign of multiplication

+

Sign of multiplication

@@ -1479,7 +1479,7 @@

Library Stdlib.Reals.RIneq

-

Order and square function

+

Order and square function

@@ -1500,7 +1500,7 @@

Library Stdlib.Reals.RIneq

-

Zero is less than one

+

Zero is less than one

@@ -1517,7 +1517,7 @@

Library Stdlib.Reals.RIneq

-

Sign of inverse

+

Sign of inverse

@@ -1536,7 +1536,7 @@

Library Stdlib.Reals.RIneq

-

Cancellation in inequalities of products

+

Cancellation in inequalities of products

@@ -1563,7 +1563,7 @@

Library Stdlib.Reals.RIneq

-

Order and inverse

+

Order and inverse

@@ -1594,7 +1594,7 @@

Library Stdlib.Reals.RIneq

-

Sign of inverse

+

Sign of inverse

@@ -1609,7 +1609,7 @@

Library Stdlib.Reals.RIneq

-

Order and subtraction

+

Order and subtraction

@@ -1653,7 +1653,7 @@

Library Stdlib.Reals.RIneq

-

Division

+

Division

@@ -1753,7 +1753,7 @@

Library Stdlib.Reals.RIneq

-

Sign of division

+

Sign of division

@@ -1778,7 +1778,7 @@

Library Stdlib.Reals.RIneq

-

Miscellaneous

+

Miscellaneous

@@ -1832,7 +1832,7 @@

Library Stdlib.Reals.RIneq

-

Injection from nat to R

+

Injection from nat to R

@@ -1931,7 +1931,7 @@

Library Stdlib.Reals.RIneq

-

Injection from positive to R

+

Injection from positive to R

@@ -2012,7 +2012,7 @@

Library Stdlib.Reals.RIneq

-

Injection from Z to R

+

Injection from Z to R

@@ -2154,7 +2154,7 @@

Library Stdlib.Reals.RIneq

-

Definitions of new types

+

Definitions of new types

@@ -2181,7 +2181,7 @@

Library Stdlib.Reals.RIneq

-

A few common instances

+

A few common instances

@@ -2197,7 +2197,7 @@

Library Stdlib.Reals.RIneq

-

Compatibility

+

Compatibility

diff --git a/v9.0/stdlib/Stdlib.Reals.ROrderedType.html b/v9.0/stdlib/Stdlib.Reals.ROrderedType.html index 0d448fa4f7..c9c8a3e3f7 100644 --- a/v9.0/stdlib/Stdlib.Reals.ROrderedType.html +++ b/v9.0/stdlib/Stdlib.Reals.ROrderedType.html @@ -54,7 +54,7 @@

Library Stdlib.Reals.ROrderedType

-

DecidableType structure for real numbers

+

DecidableType structure for real numbers

@@ -89,7 +89,7 @@

Library Stdlib.Reals.ROrderedType

and a DecidableTypeOrig.
-

OrderedType structure for binary integers

+

OrderedType structure for binary integers

@@ -137,7 +137,7 @@

Library Stdlib.Reals.ROrderedType

and a OrderedType (and also as a DecidableType).
-

An order tactic for real numbers

+

An order tactic for real numbers

diff --git a/v9.0/stdlib/Stdlib.Reals.R_Ifp.html b/v9.0/stdlib/Stdlib.Reals.R_Ifp.html index 51c5aa5706..b263da0b7c 100644 --- a/v9.0/stdlib/Stdlib.Reals.R_Ifp.html +++ b/v9.0/stdlib/Stdlib.Reals.R_Ifp.html @@ -61,7 +61,7 @@

Library Stdlib.Reals.R_Ifp

-

Fractional part

+

Fractional part

@@ -96,7 +96,7 @@

Library Stdlib.Reals.R_Ifp

-

Properties

+

Properties

diff --git a/v9.0/stdlib/Stdlib.Reals.R_sqrt.html b/v9.0/stdlib/Stdlib.Reals.R_sqrt.html index 5f8fd155d5..c62fbe9f62 100644 --- a/v9.0/stdlib/Stdlib.Reals.R_sqrt.html +++ b/v9.0/stdlib/Stdlib.Reals.R_sqrt.html @@ -54,7 +54,7 @@

Library Stdlib.Reals.R_sqrt

-

Continuous extension of Rsqrt on R

+

Continuous extension of Rsqrt on R

@@ -195,7 +195,7 @@

Library Stdlib.Reals.R_sqrt

-

Resolution of a*X^2+b*X+c=0

+

Resolution of a*X^2+b*X+c=0

diff --git a/v9.0/stdlib/Stdlib.Reals.Ranalysis1.html b/v9.0/stdlib/Stdlib.Reals.Ranalysis1.html index 9cd3e708ca..26741c4d31 100644 --- a/v9.0/stdlib/Stdlib.Reals.Ranalysis1.html +++ b/v9.0/stdlib/Stdlib.Reals.Ranalysis1.html @@ -56,7 +56,7 @@

Library Stdlib.Reals.Ranalysis1

-

Basic operations on functions

+

Basic operations on functions

@@ -105,7 +105,7 @@

Library Stdlib.Reals.Ranalysis1

-

Variations of functions

+

Variations of functions

@@ -126,7 +126,7 @@

Library Stdlib.Reals.Ranalysis1

-

Definition of continuity as a limit

+

Definition of continuity as a limit

@@ -230,7 +230,7 @@

Library Stdlib.Reals.Ranalysis1

-

Derivative's definition using Landau's kernel

+

Derivative's definition using Landau's kernel

@@ -270,7 +270,7 @@

Library Stdlib.Reals.Ranalysis1

-

Class of differential functions

+

Class of differential functions

@@ -326,7 +326,7 @@

Library Stdlib.Reals.Ranalysis1

-

Equivalence of this definition with the one using limit concept

+

Equivalence of this definition with the one using limit concept

@@ -357,7 +357,7 @@

Library Stdlib.Reals.Ranalysis1

-

derivability -> continuity

+

derivability -> continuity

@@ -375,11 +375,11 @@

Library Stdlib.Reals.Ranalysis1

-

Main rules

+

Main rules

-

Rules for derivable_pt_lim (value of the derivative at a point)

+

Rules for derivable_pt_lim (value of the derivative at a point)

@@ -457,7 +457,7 @@

Library Stdlib.Reals.Ranalysis1

-

Rules for derivable_pt (derivability at a point)

+

Rules for derivable_pt (derivability at a point)

@@ -523,7 +523,7 @@

Library Stdlib.Reals.Ranalysis1

-

Rules for derivable (derivability on whole domain)

+

Rules for derivable (derivability on whole domain)

@@ -567,7 +567,7 @@

Library Stdlib.Reals.Ranalysis1

-

Rules for derive_pt (derivative function on whole domain)

+

Rules for derive_pt (derivative function on whole domain)

@@ -637,7 +637,7 @@

Library Stdlib.Reals.Ranalysis1

-

Definition and derivative of power function with natural number exponent

+

Definition and derivative of power function with natural number exponent

@@ -671,7 +671,7 @@

Library Stdlib.Reals.Ranalysis1

-

Irrelevance of derivability proof for derivative

+

Irrelevance of derivability proof for derivative

@@ -699,7 +699,7 @@

Library Stdlib.Reals.Ranalysis1

-

Local extremum's condition

+

Local extremum's condition

diff --git a/v9.0/stdlib/Stdlib.Reals.Ranalysis5.html b/v9.0/stdlib/Stdlib.Reals.Ranalysis5.html index f61b79cec1..1e4719e336 100644 --- a/v9.0/stdlib/Stdlib.Reals.Ranalysis5.html +++ b/v9.0/stdlib/Stdlib.Reals.Ranalysis5.html @@ -62,7 +62,7 @@

Library Stdlib.Reals.Ranalysis5

-

Preliminaries lemmas

+

Preliminaries lemmas

@@ -138,11 +138,11 @@

Library Stdlib.Reals.Ranalysis5

-

The derivative of a reciprocal function

+

The derivative of a reciprocal function

-

Continuity of the reciprocal function

+

Continuity of the reciprocal function

@@ -170,7 +170,7 @@

Library Stdlib.Reals.Ranalysis5

-

Derivability of the reciprocal function

+

Derivability of the reciprocal function

@@ -244,7 +244,7 @@

Library Stdlib.Reals.Ranalysis5

-

Value of the derivative of the reciprocal function

+

Value of the derivative of the reciprocal function

@@ -320,7 +320,7 @@

Library Stdlib.Reals.Ranalysis5

-

Existence of the derivative of a function which is the limit of a sequence of functions

+

Existence of the derivative of a function which is the limit of a sequence of functions

diff --git a/v9.0/stdlib/Stdlib.Reals.Ratan.html b/v9.0/stdlib/Stdlib.Reals.Ratan.html index 5e664a6eb8..5a62f74e39 100644 --- a/v9.0/stdlib/Stdlib.Reals.Ratan.html +++ b/v9.0/stdlib/Stdlib.Reals.Ratan.html @@ -69,11 +69,11 @@

Library Stdlib.Reals.Ratan

-

Preliminaries

+

Preliminaries

-

Various generic lemmas which probably should go somewhere else

+

Various generic lemmas which probably should go somewhere else

@@ -121,11 +121,11 @@

Library Stdlib.Reals.Ratan

-

Properties of tangent

+

Properties of tangent

-

Derivative of tangent

+

Derivative of tangent

@@ -143,7 +143,7 @@

Library Stdlib.Reals.Ratan

-

Proof that tangent is a bijection

+

Proof that tangent is a bijection

@@ -193,11 +193,11 @@

Library Stdlib.Reals.Ratan

-

Definition of arctangent

+

Definition of arctangent

-

Definition of arctangent as the reciprocal function of tangent and proof of this status

+

Definition of arctangent as the reciprocal function of tangent and proof of this status

@@ -270,7 +270,7 @@

Library Stdlib.Reals.Ratan

-

Derivative of arctangent

+

Derivative of arctangent

@@ -287,7 +287,7 @@

Library Stdlib.Reals.Ratan

-

Definition of the arctangent function as the sum of the arctan power series

+

Definition of the arctangent function as the sum of the arctan power series

@@ -335,7 +335,7 @@

Library Stdlib.Reals.Ratan

-

Proof of the equivalence of the two definitions between -1 and 1

+

Proof of the equivalence of the two definitions between -1 and 1

@@ -474,7 +474,7 @@

Library Stdlib.Reals.Ratan

-

Relation between arctangent and sine and cosine

+

Relation between arctangent and sine and cosine

@@ -491,7 +491,7 @@

Library Stdlib.Reals.Ratan

-

Definition of arcsine based on arctangent

+

Definition of arcsine based on arctangent

@@ -509,7 +509,7 @@

Library Stdlib.Reals.Ratan

-

Relation between arcsin and arctangent

+

Relation between arcsin and arctangent

@@ -522,7 +522,7 @@

Library Stdlib.Reals.Ratan

-

arcsine of specific values

+

arcsine of specific values

@@ -544,7 +544,7 @@

Library Stdlib.Reals.Ratan

-

Bounds of arcsine

+

Bounds of arcsine

@@ -561,7 +561,7 @@

Library Stdlib.Reals.Ratan

-

arcsine is the left and right inverse of sine

+

arcsine is the left and right inverse of sine

@@ -578,7 +578,7 @@

Library Stdlib.Reals.Ratan

-

Relation between arcsin, cosine and tangent

+

Relation between arcsin, cosine and tangent

@@ -595,7 +595,7 @@

Library Stdlib.Reals.Ratan

-

Derivative of arcsine

+

Derivative of arcsine

@@ -612,7 +612,7 @@

Library Stdlib.Reals.Ratan

-

Definition of arccosine based on arctangent

+

Definition of arccosine based on arctangent

@@ -630,7 +630,7 @@

Library Stdlib.Reals.Ratan

-

Relation between arccosine, arcsine and arctangent

+

Relation between arccosine, arcsine and arctangent

@@ -651,7 +651,7 @@

Library Stdlib.Reals.Ratan

-

arccosine of specific values

+

arccosine of specific values

@@ -673,7 +673,7 @@

Library Stdlib.Reals.Ratan

-

Bounds of arccosine

+

Bounds of arccosine

@@ -690,7 +690,7 @@

Library Stdlib.Reals.Ratan

-

arccosine is the left and right inverse of cosine

+

arccosine is the left and right inverse of cosine

@@ -707,7 +707,7 @@

Library Stdlib.Reals.Ratan

-

Relation between arccosine, sine and tangent

+

Relation between arccosine, sine and tangent

@@ -724,7 +724,7 @@

Library Stdlib.Reals.Ratan

-

Derivative of arccosine

+

Derivative of arccosine

diff --git a/v9.0/stdlib/Stdlib.Reals.Raxioms.html b/v9.0/stdlib/Stdlib.Reals.Raxioms.html index ed79875aad..fd77077888 100644 --- a/v9.0/stdlib/Stdlib.Reals.Raxioms.html +++ b/v9.0/stdlib/Stdlib.Reals.Raxioms.html @@ -69,11 +69,11 @@

Library Stdlib.Reals.Raxioms

-

Field operations

+

Field operations

-

Addition

+

Addition

@@ -141,7 +141,7 @@

Library Stdlib.Reals.Raxioms

-

Multiplication

+

Multiplication

@@ -176,7 +176,7 @@

Library Stdlib.Reals.Raxioms

-

Distributivity

+

Distributivity

@@ -192,11 +192,11 @@

Library Stdlib.Reals.Raxioms

-

Order

+

Order

-

Lower

+

Lower

@@ -222,7 +222,7 @@

Library Stdlib.Reals.Raxioms

-

Injection from N to R

+

Injection from N to R

@@ -241,7 +241,7 @@

Library Stdlib.Reals.Raxioms

-

R Archimedean

+

R Archimedean

@@ -269,7 +269,7 @@

Library Stdlib.Reals.Raxioms

-

R Complete

+

R Complete

diff --git a/v9.0/stdlib/Stdlib.Reals.Rbasic_fun.html b/v9.0/stdlib/Stdlib.Reals.Rbasic_fun.html index cd2c8ab629..9a48f77e02 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rbasic_fun.html +++ b/v9.0/stdlib/Stdlib.Reals.Rbasic_fun.html @@ -64,7 +64,7 @@

Library Stdlib.Reals.Rbasic_fun

-

Rmin

+

Rmin

@@ -130,7 +130,7 @@

Library Stdlib.Reals.Rbasic_fun

-

Rmax

+

Rmax

@@ -202,7 +202,7 @@

Library Stdlib.Reals.Rbasic_fun

-

Rabsolu

+

Rabsolu

diff --git a/v9.0/stdlib/Stdlib.Reals.Rdefinitions.html b/v9.0/stdlib/Stdlib.Reals.Rdefinitions.html index 0bc140efff..44fa2d8a2b 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rdefinitions.html +++ b/v9.0/stdlib/Stdlib.Reals.Rdefinitions.html @@ -178,7 +178,7 @@

Library Stdlib.Reals.Rdefinitions

-

Injection from Z to R

+

Injection from Z to R

@@ -266,7 +266,7 @@

Library Stdlib.Reals.Rdefinitions

-

Number notation for constants

+

Number notation for constants

diff --git a/v9.0/stdlib/Stdlib.Reals.Rfunctions.html b/v9.0/stdlib/Stdlib.Reals.Rfunctions.html index f02141f092..82cdfb161f 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rfunctions.html +++ b/v9.0/stdlib/Stdlib.Reals.Rfunctions.html @@ -74,7 +74,7 @@

Library Stdlib.Reals.Rfunctions

-

Lemmas about factorial

+

Lemmas about factorial

@@ -91,7 +91,7 @@

Library Stdlib.Reals.Rfunctions

-

Power

+

Power

@@ -230,7 +230,7 @@

Library Stdlib.Reals.Rfunctions

-

PowerRZ

+

PowerRZ

@@ -379,7 +379,7 @@

Library Stdlib.Reals.Rfunctions

-

Sum of n first naturals

+

Sum of n first naturals

@@ -403,7 +403,7 @@

Library Stdlib.Reals.Rfunctions

-

Sum

+

Sum

@@ -431,7 +431,7 @@

Library Stdlib.Reals.Rfunctions

-

Distance in R

+

Distance in R

@@ -477,7 +477,7 @@

Library Stdlib.Reals.Rfunctions

-

Infinite Sum

+

Infinite Sum

diff --git a/v9.0/stdlib/Stdlib.Reals.Rgeom.html b/v9.0/stdlib/Stdlib.Reals.Rgeom.html index fcdbc8504f..0c92899183 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rgeom.html +++ b/v9.0/stdlib/Stdlib.Reals.Rgeom.html @@ -56,7 +56,7 @@

Library Stdlib.Reals.Rgeom

-

Distance

+

Distance

@@ -90,7 +90,7 @@

Library Stdlib.Reals.Rgeom

-

Translation

+

Translation

@@ -112,7 +112,7 @@

Library Stdlib.Reals.Rgeom

-

Rotation

+

Rotation

@@ -146,7 +146,7 @@

Library Stdlib.Reals.Rgeom

-

Similarity

+

Similarity

diff --git a/v9.0/stdlib/Stdlib.Reals.RiemannInt_SF.html b/v9.0/stdlib/Stdlib.Reals.RiemannInt_SF.html index 75318f40c7..8178d9d3e1 100644 --- a/v9.0/stdlib/Stdlib.Reals.RiemannInt_SF.html +++ b/v9.0/stdlib/Stdlib.Reals.RiemannInt_SF.html @@ -62,7 +62,7 @@

Library Stdlib.Reals.RiemannInt_SF

-

Each bounded subset of N has a maximal element

+

Each bounded subset of N has a maximal element

@@ -84,7 +84,7 @@

Library Stdlib.Reals.RiemannInt_SF

-

Step functions

+

Step functions

@@ -124,7 +124,7 @@

Library Stdlib.Reals.RiemannInt_SF

-

Class of step functions

+

Class of step functions

@@ -156,7 +156,7 @@

Library Stdlib.Reals.RiemannInt_SF

-

Integral of step functions

+

Integral of step functions

@@ -170,7 +170,7 @@

Library Stdlib.Reals.RiemannInt_SF

-

Properties of step functions

+

Properties of step functions

diff --git a/v9.0/stdlib/Stdlib.Reals.Rlimit.html b/v9.0/stdlib/Stdlib.Reals.Rlimit.html index a63c9db13c..751f6703e1 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rlimit.html +++ b/v9.0/stdlib/Stdlib.Reals.Rlimit.html @@ -62,7 +62,7 @@

Library Stdlib.Reals.Rlimit

-

Calculus

+

Calculus

@@ -100,7 +100,7 @@

Library Stdlib.Reals.Rlimit

-

Metric space

+

Metric space

@@ -119,7 +119,7 @@

Library Stdlib.Reals.Rlimit

-

Limit in Metric space

+

Limit in Metric space

@@ -138,7 +138,7 @@

Library Stdlib.Reals.Rlimit

-

R is a metric space

+

R is a metric space

@@ -154,7 +154,7 @@

Library Stdlib.Reals.Rlimit

-

Limit 1 arg

+

Limit 1 arg

diff --git a/v9.0/stdlib/Stdlib.Reals.Rlogic.html b/v9.0/stdlib/Stdlib.Reals.Rlogic.html index 7e84942d19..2c06bae070 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rlogic.html +++ b/v9.0/stdlib/Stdlib.Reals.Rlogic.html @@ -77,7 +77,7 @@

Library Stdlib.Reals.Rlogic

-

Decidability of arithmetical statements

+

Decidability of arithmetical statements

@@ -103,7 +103,7 @@

Library Stdlib.Reals.Rlogic

-

Derivability of the Archimedean axiom

+

Derivability of the Archimedean axiom

@@ -123,7 +123,7 @@

Library Stdlib.Reals.Rlogic

-

Decidability of negated formulas

+

Decidability of negated formulas

diff --git a/v9.0/stdlib/Stdlib.Reals.Rminmax.html b/v9.0/stdlib/Stdlib.Reals.Rminmax.html index 82b6f98612..a71707dca9 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rminmax.html +++ b/v9.0/stdlib/Stdlib.Reals.Rminmax.html @@ -54,7 +54,7 @@

Library Stdlib.Reals.Rminmax

-

Maximum and Minimum of two real numbers

+

Maximum and Minimum of two real numbers

@@ -111,7 +111,7 @@

Library Stdlib.Reals.Rminmax

-

Properties specific to the R domain

+

Properties specific to the R domain

diff --git a/v9.0/stdlib/Stdlib.Reals.Rpower.html b/v9.0/stdlib/Stdlib.Reals.Rpower.html index 92b80a2743..9f4decb0bb 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rpower.html +++ b/v9.0/stdlib/Stdlib.Reals.Rpower.html @@ -76,7 +76,7 @@

Library Stdlib.Reals.Rpower

-

Properties of Exp

+

Properties of Exp

@@ -129,7 +129,7 @@

Library Stdlib.Reals.Rpower

-

Properties of Ln

+

Properties of Ln

@@ -169,7 +169,7 @@

Library Stdlib.Reals.Rpower

-

Definition of Rpower

+

Definition of Rpower

@@ -181,7 +181,7 @@

Library Stdlib.Reals.Rpower

-

Properties of Rpower

+

Properties of Rpower

@@ -248,7 +248,7 @@

Library Stdlib.Reals.Rpower

-

Differentiability of Ln and Rpower

+

Differentiability of Ln and Rpower

diff --git a/v9.0/stdlib/Stdlib.Reals.Rseries.html b/v9.0/stdlib/Stdlib.Reals.Rseries.html index bb01a7a01f..1ac0f28a3a 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rseries.html +++ b/v9.0/stdlib/Stdlib.Reals.Rseries.html @@ -57,7 +57,7 @@

Library Stdlib.Reals.Rseries

-

Definition of sequence and properties

+

Definition of sequence and properties

@@ -129,7 +129,7 @@

Library Stdlib.Reals.Rseries

-

Definition of Power Series and properties

+

Definition of Power Series and properties

diff --git a/v9.0/stdlib/Stdlib.Reals.Rtopology.html b/v9.0/stdlib/Stdlib.Reals.Rtopology.html index 21ac7da5f2..d19f496bcb 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rtopology.html +++ b/v9.0/stdlib/Stdlib.Reals.Rtopology.html @@ -58,7 +58,7 @@

Library Stdlib.Reals.Rtopology

-

General definitions and propositions

+

General definitions and propositions

@@ -306,7 +306,7 @@

Library Stdlib.Reals.Rtopology

-

Proof of Bolzano-Weierstrass theorem

+

Proof of Bolzano-Weierstrass theorem

@@ -379,7 +379,7 @@

Library Stdlib.Reals.Rtopology

-

Proof of Heine's theorem

+

Proof of Heine's theorem

diff --git a/v9.0/stdlib/Stdlib.Reals.Rtrigo1.html b/v9.0/stdlib/Stdlib.Reals.Rtrigo1.html index 4d4ed8fcf9..0f8e20a6c4 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rtrigo1.html +++ b/v9.0/stdlib/Stdlib.Reals.Rtrigo1.html @@ -165,7 +165,7 @@

Library Stdlib.Reals.Rtrigo1

-

Some properties of cos, sin and tan

+

Some properties of cos, sin and tan

@@ -259,7 +259,7 @@

Library Stdlib.Reals.Rtrigo1

-

Using series definitions of cos and sin

+

Using series definitions of cos and sin

@@ -293,7 +293,7 @@

Library Stdlib.Reals.Rtrigo1

-

Increasing and decreasing of cos and sin

+

Increasing and decreasing of cos and sin

diff --git a/v9.0/stdlib/Stdlib.Reals.Rtrigo_def.html b/v9.0/stdlib/Stdlib.Reals.Rtrigo_def.html index 89d4203ced..bdf24533ac 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rtrigo_def.html +++ b/v9.0/stdlib/Stdlib.Reals.Rtrigo_def.html @@ -54,7 +54,7 @@

Library Stdlib.Reals.Rtrigo_def

-

Definition of exponential

+

Definition of exponential

@@ -80,7 +80,7 @@

Library Stdlib.Reals.Rtrigo_def

-

Definition of hyperbolic functions

+

Definition of hyperbolic functions

@@ -154,7 +154,7 @@

Library Stdlib.Reals.Rtrigo_def

-

Properties

+

Properties

diff --git a/v9.0/stdlib/Stdlib.Reals.Rtrigo_facts.html b/v9.0/stdlib/Stdlib.Reals.Rtrigo_facts.html index 25545359e1..86f7a91bd1 100644 --- a/v9.0/stdlib/Stdlib.Reals.Rtrigo_facts.html +++ b/v9.0/stdlib/Stdlib.Reals.Rtrigo_facts.html @@ -60,7 +60,7 @@

Library Stdlib.Reals.Rtrigo_facts

-

Bounds of expressions with trigonometric functions

+

Bounds of expressions with trigonometric functions

@@ -77,11 +77,11 @@

Library Stdlib.Reals.Rtrigo_facts

-

Express trigonometric functions with each other

+

Express trigonometric functions with each other

-

Express sin and cos with each other

+

Express sin and cos with each other

@@ -114,7 +114,7 @@

Library Stdlib.Reals.Rtrigo_facts

-

Express tan with sin and cos

+

Express tan with sin and cos

@@ -147,7 +147,7 @@

Library Stdlib.Reals.Rtrigo_facts

-

Express sin and cos with tan

+

Express sin and cos with tan

@@ -164,7 +164,7 @@

Library Stdlib.Reals.Rtrigo_facts

-

Additional shift lemmas for sin, cos, tan

+

Additional shift lemmas for sin, cos, tan

diff --git a/v9.0/stdlib/Stdlib.Relations.Operators_Properties.html b/v9.0/stdlib/Stdlib.Relations.Operators_Properties.html index 45d5ae02a0..ec164bf752 100644 --- a/v9.0/stdlib/Stdlib.Relations.Operators_Properties.html +++ b/v9.0/stdlib/Stdlib.Relations.Operators_Properties.html @@ -48,8 +48,8 @@

Library Stdlib.Relations.Operators_Properties

-

Some properties of the operators on relations

-

Initial version by Bruno Barras

+

Some properties of the operators on relations

+

Initial version by Bruno Barras

@@ -184,12 +184,12 @@

Library Stdlib.Relations.Operators_Properties

-

Equivalences between the different definition of the reflexive,

+

Equivalences between the different definition of the reflexive,

symmetric, transitive closures
-

Contributed by P. Castéran

+

Contributed by P. Castéran

diff --git a/v9.0/stdlib/Stdlib.Relations.Relation_Operators.html b/v9.0/stdlib/Stdlib.Relations.Relation_Operators.html index 3e51774176..ec113f2c9f 100644 --- a/v9.0/stdlib/Stdlib.Relations.Relation_Operators.html +++ b/v9.0/stdlib/Stdlib.Relations.Relation_Operators.html @@ -48,14 +48,14 @@

Library Stdlib.Relations.Relation_Operators

-

Some operators on relations

-

Initial authors: Bruno Barras, Cristina Cornes

-

-

Some of the initial definitions were taken from :

-

Constructing Recursion Operators in Type Theory

-

L. Paulson JSC (1986) 2, 325-355

-

-

Further extensions by Pierre Castéran

+

Some operators on relations

+

Initial authors: Bruno Barras, Cristina Cornes

+

+

Some of the initial definitions were taken from :

+

Constructing Recursion Operators in Type Theory

+

L. Paulson JSC (1986) 2, 325-355

+

+

Further extensions by Pierre Castéran

@@ -67,7 +67,7 @@

Library Stdlib.Relations.Relation_Operators

-

Transitive closure

+

Transitive closure

@@ -123,7 +123,7 @@

Library Stdlib.Relations.Relation_Operators

-

Reflexive closure

+

Reflexive closure

@@ -153,7 +153,7 @@

Library Stdlib.Relations.Relation_Operators

-

Reflexive-transitive closure

+

Reflexive-transitive closure

@@ -213,7 +213,7 @@

Library Stdlib.Relations.Relation_Operators

-

Reflexive-symmetric-transitive closure

+

Reflexive-symmetric-transitive closure

@@ -275,7 +275,7 @@

Library Stdlib.Relations.Relation_Operators

-

Converse of a relation

+

Converse of a relation

@@ -293,7 +293,7 @@

Library Stdlib.Relations.Relation_Operators

-

Union of relations

+

Union of relations

@@ -311,7 +311,7 @@

Library Stdlib.Relations.Relation_Operators

-

Disjoint union of relations

+

Disjoint union of relations

@@ -335,7 +335,7 @@

Library Stdlib.Relations.Relation_Operators

-

Lexicographic order on dependent pairs

+

Lexicographic order on dependent pairs

@@ -368,7 +368,7 @@

Library Stdlib.Relations.Relation_Operators

-

Lexicographic order on pairs

+

Lexicographic order on pairs

@@ -403,7 +403,7 @@

Library Stdlib.Relations.Relation_Operators

-

Product of relations

+

Product of relations

@@ -429,7 +429,7 @@

Library Stdlib.Relations.Relation_Operators

-

Multiset of two relations

+

Multiset of two relations

diff --git a/v9.0/stdlib/Stdlib.Sorting.CPermutation.html b/v9.0/stdlib/Stdlib.Sorting.CPermutation.html index a4f1d0cc23..fb6346c308 100644 --- a/v9.0/stdlib/Stdlib.Sorting.CPermutation.html +++ b/v9.0/stdlib/Stdlib.Sorting.CPermutation.html @@ -48,7 +48,7 @@

Library Stdlib.Sorting.CPermutation

-

Circular Shifts (aka Cyclic Permutations)

+

Circular Shifts (aka Cyclic Permutations)

diff --git a/v9.0/stdlib/Stdlib.Sorting.Heap.html b/v9.0/stdlib/Stdlib.Sorting.Heap.html index 74d8c44c56..8cdc18ce29 100644 --- a/v9.0/stdlib/Stdlib.Sorting.Heap.html +++ b/v9.0/stdlib/Stdlib.Sorting.Heap.html @@ -73,11 +73,11 @@

Library Stdlib.Sorting.Heap

-

Trees and heap trees

+

Trees and heap trees

-

Definition of trees over an ordered set

+

Definition of trees over an ordered set

@@ -142,7 +142,7 @@

Library Stdlib.Sorting.Heap

-

The heap property

+

The heap property

@@ -194,7 +194,7 @@

Library Stdlib.Sorting.Heap

-

Merging two sorted lists

+

Merging two sorted lists

@@ -226,7 +226,7 @@

Library Stdlib.Sorting.Heap

-

From trees to multisets

+

From trees to multisets

@@ -262,11 +262,11 @@

Library Stdlib.Sorting.Heap

-

From lists to sorted lists

+

From lists to sorted lists

-

Specification of heap insertion

+

Specification of heap insertion

@@ -288,7 +288,7 @@

Library Stdlib.Sorting.Heap

-

Building a heap from a list

+

Building a heap from a list

@@ -308,7 +308,7 @@

Library Stdlib.Sorting.Heap

-

Building the sorted list

+

Building the sorted list

@@ -329,7 +329,7 @@

Library Stdlib.Sorting.Heap

-

Specification of treesort

+

Specification of treesort

diff --git a/v9.0/stdlib/Stdlib.Sorting.PermutSetoid.html b/v9.0/stdlib/Stdlib.Sorting.PermutSetoid.html index 68585daaa1..5f0bb7c06f 100644 --- a/v9.0/stdlib/Stdlib.Sorting.PermutSetoid.html +++ b/v9.0/stdlib/Stdlib.Sorting.PermutSetoid.html @@ -88,7 +88,7 @@

Library Stdlib.Sorting.PermutSetoid

-

From lists to multisets

+

From lists to multisets

@@ -127,7 +127,7 @@

Library Stdlib.Sorting.PermutSetoid

-

permutation: definition and basic properties

+

permutation: definition and basic properties

@@ -201,7 +201,7 @@

Library Stdlib.Sorting.PermutSetoid

-

Some inversion results.

+

Some inversion results.

diff --git a/v9.0/stdlib/Stdlib.Sorting.Permutation.html b/v9.0/stdlib/Stdlib.Sorting.Permutation.html index 812e61f0e9..d63eaa0150 100644 --- a/v9.0/stdlib/Stdlib.Sorting.Permutation.html +++ b/v9.0/stdlib/Stdlib.Sorting.Permutation.html @@ -48,7 +48,7 @@

Library Stdlib.Sorting.Permutation

-

List permutations as a composition of adjacent transpositions

+

List permutations as a composition of adjacent transpositions

diff --git a/v9.0/stdlib/Stdlib.Strings.Ascii.html b/v9.0/stdlib/Stdlib.Strings.Ascii.html index 6c183554a1..ada657720c 100644 --- a/v9.0/stdlib/Stdlib.Strings.Ascii.html +++ b/v9.0/stdlib/Stdlib.Strings.Ascii.html @@ -61,7 +61,7 @@

Library Stdlib.Strings.Ascii

-

Definition of ascii characters

+

Definition of ascii characters

@@ -141,7 +141,7 @@

Library Stdlib.Strings.Ascii

-

Conversion between natural numbers modulo 256 and ascii characters

+

Conversion between natural numbers modulo 256 and ascii characters

@@ -283,7 +283,7 @@

Library Stdlib.Strings.Ascii

-

Concrete syntax

+

Concrete syntax

diff --git a/v9.0/stdlib/Stdlib.Strings.PString.html b/v9.0/stdlib/Stdlib.Strings.PString.html index 5857d14907..66e53f29dd 100644 --- a/v9.0/stdlib/Stdlib.Strings.PString.html +++ b/v9.0/stdlib/Stdlib.Strings.PString.html @@ -127,7 +127,7 @@

Library Stdlib.Strings.PString

-

Properties of string length

+

Properties of string length

@@ -168,7 +168,7 @@

Library Stdlib.Strings.PString

-

Properties of string get

+

Properties of string get

@@ -211,7 +211,7 @@

Library Stdlib.Strings.PString

-

Properties of string comparison

+

Properties of string comparison

@@ -292,7 +292,7 @@

Library Stdlib.Strings.PString

-

Properties of make

+

Properties of make

@@ -304,7 +304,7 @@

Library Stdlib.Strings.PString

-

Properties of cat

+

Properties of cat

@@ -326,7 +326,7 @@

Library Stdlib.Strings.PString

-

Properties of sub

+

Properties of sub

@@ -374,7 +374,7 @@

Library Stdlib.Strings.PString

-

Ordered type

+

Ordered type

diff --git a/v9.0/stdlib/Stdlib.Strings.String.html b/v9.0/stdlib/Stdlib.Strings.String.html index f8119eb947..7aa08bc6d3 100644 --- a/v9.0/stdlib/Stdlib.Strings.String.html +++ b/v9.0/stdlib/Stdlib.Strings.String.html @@ -64,7 +64,7 @@

Library Stdlib.Strings.String

-

Definition of strings

+

Definition of strings

@@ -135,7 +135,7 @@

Library Stdlib.Strings.String

-

Compare strings lexicographically

+

Compare strings lexicographically

@@ -185,7 +185,7 @@

Library Stdlib.Strings.String

-

Concatenation of strings

+

Concatenation of strings

@@ -276,7 +276,7 @@

Library Stdlib.Strings.String

-

Substrings

+

Substrings

@@ -325,7 +325,7 @@

Library Stdlib.Strings.String

-

Concatenating lists of strings

+

Concatenating lists of strings

@@ -346,7 +346,7 @@

Library Stdlib.Strings.String

-

Test functions

+

Test functions

@@ -498,7 +498,7 @@

Library Stdlib.Strings.String

-

Conversion to/from list ascii and list byte

+

Conversion to/from list ascii and list byte

@@ -541,7 +541,7 @@

Library Stdlib.Strings.String

-

Concrete syntax

+

Concrete syntax

diff --git a/v9.0/stdlib/Stdlib.Structures.DecidableType.html b/v9.0/stdlib/Stdlib.Structures.DecidableType.html index 95606d0c41..ef4184788e 100644 --- a/v9.0/stdlib/Stdlib.Structures.DecidableType.html +++ b/v9.0/stdlib/Stdlib.Structures.DecidableType.html @@ -59,7 +59,7 @@

Library Stdlib.Structures.DecidableType

FSets and FMap. Please use Structures/Equalities.v directly now.
-

Types with Equalities, and nothing more (for subtyping purpose)

+

Types with Equalities, and nothing more (for subtyping purpose)

@@ -71,7 +71,7 @@

Library Stdlib.Structures.DecidableType

-

Types with decidable Equalities (but no ordering)

+

Types with decidable Equalities (but no ordering)

@@ -83,7 +83,7 @@

Library Stdlib.Structures.DecidableType

-

Additional notions about keys and datas used in FMap

+

Additional notions about keys and datas used in FMap

diff --git a/v9.0/stdlib/Stdlib.Structures.DecidableTypeEx.html b/v9.0/stdlib/Stdlib.Structures.DecidableTypeEx.html index 5cf8937e25..bb6b9b8890 100644 --- a/v9.0/stdlib/Stdlib.Structures.DecidableTypeEx.html +++ b/v9.0/stdlib/Stdlib.Structures.DecidableTypeEx.html @@ -56,7 +56,7 @@

Library Stdlib.Structures.DecidableTypeEx

FSets and FMap. Please use Structures/Equalities.v directly now.
-

Examples of Decidable Type structures.

+

Examples of Decidable Type structures.

diff --git a/v9.0/stdlib/Stdlib.Structures.Equalities.html b/v9.0/stdlib/Stdlib.Structures.Equalities.html index f0c932be8f..dbfd3b79df 100644 --- a/v9.0/stdlib/Stdlib.Structures.Equalities.html +++ b/v9.0/stdlib/Stdlib.Structures.Equalities.html @@ -68,7 +68,7 @@

Library Stdlib.Structures.Equalities

-

Structure with just a base type t

+

Structure with just a base type t

@@ -82,7 +82,7 @@

Library Stdlib.Structures.Equalities

-

Structure with an equality relation eq

+

Structure with an equality relation eq

@@ -108,7 +108,7 @@

Library Stdlib.Structures.Equalities

-

Specification of the equality via the Equivalence type class

+

Specification of the equality via the Equivalence type class

@@ -123,7 +123,7 @@

Library Stdlib.Structures.Equalities

-

Earlier specification of equality by three separate lemmas.

+

Earlier specification of equality by three separate lemmas.

@@ -143,7 +143,7 @@

Library Stdlib.Structures.Equalities

-

Types with decidable equality

+

Types with decidable equality

@@ -157,7 +157,7 @@

Library Stdlib.Structures.Equalities

-

Boolean Equality

+

Boolean Equality

@@ -252,7 +252,7 @@

Library Stdlib.Structures.Equalities

-

Compatibility wrapper from/to the old version of

+

Compatibility wrapper from/to the old version of

EqualityType and DecidableType
@@ -291,7 +291,7 @@

Library Stdlib.Structures.Equalities

-

Having eq_dec is equivalent to having eqb and its spec.

+

Having eq_dec is equivalent to having eqb and its spec.

@@ -389,7 +389,7 @@

Library Stdlib.Structures.Equalities

-

UsualDecidableType

+

UsualDecidableType

diff --git a/v9.0/stdlib/Stdlib.Structures.EqualitiesFacts.html b/v9.0/stdlib/Stdlib.Structures.EqualitiesFacts.html index 742448106c..914d816b9d 100644 --- a/v9.0/stdlib/Stdlib.Structures.EqualitiesFacts.html +++ b/v9.0/stdlib/Stdlib.Structures.EqualitiesFacts.html @@ -54,7 +54,7 @@

Library Stdlib.Structures.EqualitiesFacts

-

Keys and datas used in the future MMaps

+

Keys and datas used in the future MMaps

@@ -226,7 +226,7 @@

Library Stdlib.Structures.EqualitiesFacts

-

PairDecidableType

+

PairDecidableType

diff --git a/v9.0/stdlib/Stdlib.Structures.GenericMinMax.html b/v9.0/stdlib/Stdlib.Structures.GenericMinMax.html index 3e2ceeb850..d6b805110c 100644 --- a/v9.0/stdlib/Stdlib.Structures.GenericMinMax.html +++ b/v9.0/stdlib/Stdlib.Structures.GenericMinMax.html @@ -51,11 +51,11 @@

Library Stdlib.Structures.GenericMinMax

-

A Generic construction of min and max

+

A Generic construction of min and max

-

First, an interface for types with max and/or min

+

First, an interface for types with max and/or min

@@ -81,7 +81,7 @@

Library Stdlib.Structures.GenericMinMax

-

Any OrderedTypeFull can be equipped by max and min

+

Any OrderedTypeFull can be equipped by max and min

based on the compare function.
@@ -122,7 +122,7 @@

Library Stdlib.Structures.GenericMinMax

-

Consequences of the minimalist interface: facts about max and min.

+

Consequences of the minimalist interface: facts about max and min.

@@ -200,7 +200,7 @@

Library Stdlib.Structures.GenericMinMax

-

Semi-lattice algebraic properties of max

+

Semi-lattice algebraic properties of max

@@ -227,7 +227,7 @@

Library Stdlib.Structures.GenericMinMax

-

Least-upper bound properties of max

+

Least-upper bound properties of max

@@ -386,7 +386,7 @@

Library Stdlib.Structures.GenericMinMax

-

Combined properties of min and max

+

Combined properties of min and max

@@ -468,7 +468,7 @@

Library Stdlib.Structures.GenericMinMax

-

Properties requiring a decidable order

+

Properties requiring a decidable order

@@ -548,7 +548,7 @@

Library Stdlib.Structures.GenericMinMax

-

When the equality is Leibniz, we can skip a few Proper precondition.

+

When the equality is Leibniz, we can skip a few Proper precondition.

diff --git a/v9.0/stdlib/Stdlib.Structures.OrderedType.html b/v9.0/stdlib/Stdlib.Structures.OrderedType.html index 828ef06da1..74926ed95a 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrderedType.html +++ b/v9.0/stdlib/Stdlib.Structures.OrderedType.html @@ -56,7 +56,7 @@

Library Stdlib.Structures.OrderedType

FSets and FMap. Please use Structures/Orders.v directly now.
-

Ordered types

+

Ordered types

@@ -137,7 +137,7 @@

Library Stdlib.Structures.OrderedType

-

Ordered types properties

+

Ordered types properties

diff --git a/v9.0/stdlib/Stdlib.Structures.OrderedTypeAlt.html b/v9.0/stdlib/Stdlib.Structures.OrderedTypeAlt.html index 93195e84bc..e6069ae15e 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrderedTypeAlt.html +++ b/v9.0/stdlib/Stdlib.Structures.OrderedTypeAlt.html @@ -49,7 +49,7 @@

Library Stdlib.Structures.OrderedTypeAlt

-

An alternative (but equivalent) presentation for an Ordered Type

+

An alternative (but equivalent) presentation for an Ordered Type

inferface.
diff --git a/v9.0/stdlib/Stdlib.Structures.OrderedTypeEx.html b/v9.0/stdlib/Stdlib.Structures.OrderedTypeEx.html index 2720156147..676ab279ae 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrderedTypeEx.html +++ b/v9.0/stdlib/Stdlib.Structures.OrderedTypeEx.html @@ -55,7 +55,7 @@

Library Stdlib.Structures.OrderedTypeEx

-

Examples of Ordered Type structures.

+

Examples of Ordered Type structures.

diff --git a/v9.0/stdlib/Stdlib.Structures.Orders.html b/v9.0/stdlib/Stdlib.Structures.Orders.html index 411779cd1a..d888863970 100644 --- a/v9.0/stdlib/Stdlib.Structures.Orders.html +++ b/v9.0/stdlib/Stdlib.Structures.Orders.html @@ -52,7 +52,7 @@

Library Stdlib.Structures.Orders

-

Ordered types

+

Ordered types

@@ -187,7 +187,7 @@

Library Stdlib.Structures.Orders

DecidableType.
-

Versions with eq being the usual Leibniz equality of Coq

+

Versions with eq being the usual Leibniz equality of Coq

@@ -219,7 +219,7 @@

Library Stdlib.Structures.Orders

-

Purely logical versions

+

Purely logical versions

@@ -242,7 +242,7 @@

Library Stdlib.Structures.Orders

-

Conversions

+

Conversions

@@ -303,7 +303,7 @@

Library Stdlib.Structures.Orders

-

Versions with boolean comparisons

+

Versions with boolean comparisons

@@ -405,7 +405,7 @@

Library Stdlib.Structures.Orders

-

From OrderedTypeFull to TotalTransitiveLeBool

+

From OrderedTypeFull to TotalTransitiveLeBool

@@ -436,7 +436,7 @@

Library Stdlib.Structures.Orders

-

From TotalTransitiveLeBool to OrderedTypeFull

+

From TotalTransitiveLeBool to OrderedTypeFull

diff --git a/v9.0/stdlib/Stdlib.Structures.OrdersAlt.html b/v9.0/stdlib/Stdlib.Structures.OrdersAlt.html index e43bc8b569..5523bf89f6 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrdersAlt.html +++ b/v9.0/stdlib/Stdlib.Structures.OrdersAlt.html @@ -54,12 +54,12 @@

Library Stdlib.Structures.OrdersAlt

-

Some alternative (but equivalent) presentations for an Ordered Type

+

Some alternative (but equivalent) presentations for an Ordered Type

inferface.
-

The original interface

+

The original interface

@@ -71,7 +71,7 @@

Library Stdlib.Structures.OrdersAlt

-

An interface based on compare

+

An interface based on compare

@@ -101,7 +101,7 @@

Library Stdlib.Structures.OrdersAlt

-

From OrderedTypeOrig to OrderedType.

+

From OrderedTypeOrig to OrderedType.

@@ -140,7 +140,7 @@

Library Stdlib.Structures.OrdersAlt

-

From OrderedType to OrderedTypeOrig.

+

From OrderedType to OrderedTypeOrig.

@@ -169,7 +169,7 @@

Library Stdlib.Structures.OrdersAlt

-

From OrderedTypeAlt to OrderedType.

+

From OrderedTypeAlt to OrderedType.

diff --git a/v9.0/stdlib/Stdlib.Structures.OrdersEx.html b/v9.0/stdlib/Stdlib.Structures.OrdersEx.html index 66f69d3dd9..390e4d4d2a 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrdersEx.html +++ b/v9.0/stdlib/Stdlib.Structures.OrdersEx.html @@ -55,7 +55,7 @@

Library Stdlib.Structures.OrdersEx

-

Examples of Ordered Type structures.

+

Examples of Ordered Type structures.

diff --git a/v9.0/stdlib/Stdlib.Structures.OrdersFacts.html b/v9.0/stdlib/Stdlib.Structures.OrdersFacts.html index 0caf7bf0a4..fd5ce206db 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrdersFacts.html +++ b/v9.0/stdlib/Stdlib.Structures.OrdersFacts.html @@ -55,7 +55,7 @@

Library Stdlib.Structures.OrdersFacts

-

Properties of compare

+

Properties of compare

@@ -104,7 +104,7 @@

Library Stdlib.Structures.OrdersFacts

-

Properties of OrderedTypeFull

+

Properties of OrderedTypeFull

@@ -164,7 +164,7 @@

Library Stdlib.Structures.OrdersFacts

-

Properties of OrderedType

+

Properties of OrderedType

@@ -259,7 +259,7 @@

Library Stdlib.Structures.OrdersFacts

-

Tests of the order tactic

+

Tests of the order tactic

@@ -297,7 +297,7 @@

Library Stdlib.Structures.OrdersFacts

-

Reversed OrderedTypeFull.

+

Reversed OrderedTypeFull.

@@ -348,7 +348,7 @@

Library Stdlib.Structures.OrdersFacts

-

Order relations derived from a compare function.

+

Order relations derived from a compare function.

diff --git a/v9.0/stdlib/Stdlib.Structures.OrdersLists.html b/v9.0/stdlib/Stdlib.Structures.OrdersLists.html index ff16730a2d..2e4c11f051 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrdersLists.html +++ b/v9.0/stdlib/Stdlib.Structures.OrdersLists.html @@ -54,7 +54,7 @@

Library Stdlib.Structures.OrdersLists

-

Specialization of results about lists modulo.

+

Specialization of results about lists modulo.

@@ -109,7 +109,7 @@

Library Stdlib.Structures.OrdersLists

-

Results about keys and data as manipulated in the future MMaps.

+

Results about keys and data as manipulated in the future MMaps.

diff --git a/v9.0/stdlib/Stdlib.Structures.OrdersTac.html b/v9.0/stdlib/Stdlib.Structures.OrdersTac.html index 698618aa25..0ac460b400 100644 --- a/v9.0/stdlib/Stdlib.Structures.OrdersTac.html +++ b/v9.0/stdlib/Stdlib.Structures.OrdersTac.html @@ -52,7 +52,7 @@

Library Stdlib.Structures.OrdersTac

-

The order tactic

+

The order tactic

@@ -91,7 +91,7 @@

Library Stdlib.Structures.OrdersTac

-

The tactic requirements : a total order

+

The tactic requirements : a total order

@@ -127,7 +127,7 @@

Library Stdlib.Structures.OrdersTac

-

Properties that will be used by the order tactic

+

Properties that will be used by the order tactic

@@ -237,7 +237,7 @@

Library Stdlib.Structures.OrdersTac

-

MakeOrderTac : The functor providing the order tactic.

+

MakeOrderTac : The functor providing the order tactic.

diff --git a/v9.0/stdlib/Stdlib.Vectors.VectorDef.html b/v9.0/stdlib/Stdlib.Vectors.VectorDef.html index fe7a610784..9679c9633f 100644 --- a/v9.0/stdlib/Stdlib.Vectors.VectorDef.html +++ b/v9.0/stdlib/Stdlib.Vectors.VectorDef.html @@ -436,7 +436,7 @@

Library Stdlib.Vectors.VectorDef

-

Here are special non dependent useful instantiation of induction schemes

+

Here are special non dependent useful instantiation of induction schemes

@@ -563,7 +563,7 @@

Library Stdlib.Vectors.VectorDef

-

vector <=> list functions

+

vector <=> list functions

diff --git a/v9.0/stdlib/Stdlib.Vectors.VectorSpec.html b/v9.0/stdlib/Stdlib.Vectors.VectorSpec.html index 93a2db706a..384f74786a 100644 --- a/v9.0/stdlib/Stdlib.Vectors.VectorSpec.html +++ b/v9.0/stdlib/Stdlib.Vectors.VectorSpec.html @@ -94,7 +94,7 @@

Library Stdlib.Vectors.VectorSpec

is true for the one that use lt
-

Properties of nth and nth_order

+

Properties of nth and nth_order

@@ -135,7 +135,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of replace

+

Properties of replace

@@ -181,7 +181,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of const

+

Properties of const

@@ -196,7 +196,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of map

+

Properties of map

@@ -237,7 +237,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of fold_left

+

Properties of fold_left

@@ -251,7 +251,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of take

+

Properties of take

@@ -273,7 +273,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of uncons and splitat

+

Properties of uncons and splitat

@@ -304,7 +304,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of In

+

Properties of In

@@ -317,7 +317,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of Forall and Forall2

+

Properties of Forall and Forall2

@@ -371,7 +371,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of shiftin and shiftrepeat

+

Properties of shiftin and shiftrepeat

@@ -410,7 +410,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of rev

+

Properties of rev

@@ -448,7 +448,7 @@

Library Stdlib.Vectors.VectorSpec

-

Properties of to_list

+

Properties of to_list

diff --git a/v9.0/stdlib/Stdlib.ZArith.BinInt.html b/v9.0/stdlib/Stdlib.ZArith.BinInt.html index 965d2c7e34..6f794f8e16 100644 --- a/v9.0/stdlib/Stdlib.ZArith.BinInt.html +++ b/v9.0/stdlib/Stdlib.ZArith.BinInt.html @@ -54,7 +54,7 @@

Library Stdlib.ZArith.BinInt

-

Binary Integers

+

Binary Integers

@@ -89,7 +89,7 @@

Library Stdlib.ZArith.BinInt

-

Definitions of operations, now in a separate file

+

Definitions of operations, now in a separate file

@@ -121,7 +121,7 @@

Library Stdlib.ZArith.BinInt

-

Logic Predicates

+

Logic Predicates

@@ -159,7 +159,7 @@

Library Stdlib.ZArith.BinInt

-

Decidability of equality.

+

Decidability of equality.

@@ -171,7 +171,7 @@

Library Stdlib.ZArith.BinInt

-

Proofs of morphisms, obvious since eq is Leibniz

+

Proofs of morphisms, obvious since eq is Leibniz

@@ -196,7 +196,7 @@

Library Stdlib.ZArith.BinInt

-

Properties of pos_sub

+

Properties of pos_sub

@@ -267,7 +267,7 @@

Library Stdlib.ZArith.BinInt

-

Operations and constants

+

Operations and constants

@@ -285,7 +285,7 @@

Library Stdlib.ZArith.BinInt

-

Addition is commutative

+

Addition is commutative

@@ -297,7 +297,7 @@

Library Stdlib.ZArith.BinInt

-

Opposite distributes over addition

+

Opposite distributes over addition

@@ -309,7 +309,7 @@

Library Stdlib.ZArith.BinInt

-

Opposite is injective

+

Opposite is injective

@@ -321,7 +321,7 @@

Library Stdlib.ZArith.BinInt

-

Addition is associative

+

Addition is associative

@@ -343,7 +343,7 @@

Library Stdlib.ZArith.BinInt

-

Opposite is inverse for addition

+

Opposite is inverse for addition

@@ -355,7 +355,7 @@

Library Stdlib.ZArith.BinInt

-

Multiplication and Opposite

+

Multiplication and Opposite

@@ -367,7 +367,7 @@

Library Stdlib.ZArith.BinInt

-

Distributivity of multiplication over addition

+

Distributivity of multiplication over addition

@@ -386,11 +386,11 @@

Library Stdlib.ZArith.BinInt

-

Proofs of specifications

+

Proofs of specifications

-

Specification of constants

+

Specification of constants

@@ -405,7 +405,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of addition

+

Specification of addition

@@ -420,7 +420,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of opposite

+

Specification of opposite

@@ -435,7 +435,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of successor and predecessor

+

Specification of successor and predecessor

@@ -453,7 +453,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of subtraction

+

Specification of subtraction

@@ -468,7 +468,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of multiplication

+

Specification of multiplication

@@ -483,7 +483,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of comparisons and order

+

Specification of comparisons and order

@@ -575,7 +575,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of minimum and maximum

+

Specification of minimum and maximum

@@ -596,7 +596,7 @@

Library Stdlib.ZArith.BinInt

-

Induction principles based on successor / predecessor

+

Induction principles based on successor / predecessor

@@ -637,7 +637,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of absolute value

+

Specification of absolute value

@@ -652,7 +652,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of sign

+

Specification of sign

@@ -670,7 +670,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of power

+

Specification of power

@@ -699,7 +699,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of square

+

Specification of square

@@ -711,7 +711,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of square root

+

Specification of square root

@@ -734,7 +734,7 @@

Library Stdlib.ZArith.BinInt

-

Specification of logarithm

+

Specification of logarithm

@@ -763,7 +763,7 @@

Library Stdlib.ZArith.BinInt

-

Multiplication and Doubling

+

Multiplication and Doubling

@@ -781,7 +781,7 @@

Library Stdlib.ZArith.BinInt

-

Correctness proofs for Trunc division

+

Correctness proofs for Trunc division

@@ -813,7 +813,7 @@

Library Stdlib.ZArith.BinInt

-

Correctness proofs for Floor division

+

Correctness proofs for Floor division

@@ -846,7 +846,7 @@

Library Stdlib.ZArith.BinInt

-

Extra properties about divide

+

Extra properties about divide

@@ -864,7 +864,7 @@

Library Stdlib.ZArith.BinInt

-

Correctness proofs for gcd

+

Correctness proofs for gcd

@@ -905,7 +905,7 @@

Library Stdlib.ZArith.BinInt

-

Extra properties about testbit

+

Extra properties about testbit

@@ -930,7 +930,7 @@

Library Stdlib.ZArith.BinInt

-

Proofs of specifications for bitwise operations

+

Proofs of specifications for bitwise operations

@@ -1109,7 +1109,7 @@

Library Stdlib.ZArith.BinInt

-

Comparison and opposite

+

Comparison and opposite

@@ -1121,7 +1121,7 @@

Library Stdlib.ZArith.BinInt

-

Comparison and addition

+

Comparison and addition

@@ -1133,7 +1133,7 @@

Library Stdlib.ZArith.BinInt

-

testbit in terms of comparison.

+

testbit in terms of comparison.

diff --git a/v9.0/stdlib/Stdlib.ZArith.BinIntDef.html b/v9.0/stdlib/Stdlib.ZArith.BinIntDef.html index d0d4b749d5..dc3b2084f0 100644 --- a/v9.0/stdlib/Stdlib.ZArith.BinIntDef.html +++ b/v9.0/stdlib/Stdlib.ZArith.BinIntDef.html @@ -61,7 +61,7 @@

Library Stdlib.ZArith.BinIntDef

-

Binary Integers, Definitions of Operations

+

Binary Integers, Definitions of Operations

@@ -82,7 +82,7 @@

Library Stdlib.ZArith.BinIntDef

-

Nicer names Z.pos and Z.neg for constructors

+

Nicer names Z.pos and Z.neg for constructors

@@ -95,7 +95,7 @@

Library Stdlib.ZArith.BinIntDef

-

Constants

+

Constants

@@ -109,7 +109,7 @@

Library Stdlib.ZArith.BinIntDef

-

Successor

+

Successor

@@ -121,7 +121,7 @@

Library Stdlib.ZArith.BinIntDef

-

Predecessor

+

Predecessor

@@ -133,7 +133,7 @@

Library Stdlib.ZArith.BinIntDef

-

Square

+

Square

@@ -150,7 +150,7 @@

Library Stdlib.ZArith.BinIntDef

-

Sign function

+

Sign function

@@ -201,7 +201,7 @@

Library Stdlib.ZArith.BinIntDef

-

Absolute value

+

Absolute value

@@ -218,7 +218,7 @@

Library Stdlib.ZArith.BinIntDef

-

Conversions

+

Conversions

@@ -333,7 +333,7 @@

Library Stdlib.ZArith.BinIntDef

-

Iteration of a function

+

Iteration of a function

@@ -358,7 +358,7 @@

Library Stdlib.ZArith.BinIntDef

-

Parity functions

+

Parity functions

@@ -376,7 +376,7 @@

Library Stdlib.ZArith.BinIntDef

-

Division by two

+

Division by two

@@ -403,7 +403,7 @@

Library Stdlib.ZArith.BinIntDef

NB: Z.quot2 used to be named Z.div2 in Coq <= 8.3
-

Base-2 logarithm

+

Base-2 logarithm

@@ -420,7 +420,7 @@

Library Stdlib.ZArith.BinIntDef

-

Square root

+

Square root

@@ -436,7 +436,7 @@

Library Stdlib.ZArith.BinIntDef

-

Greatest Common Divisor

+

Greatest Common Divisor

@@ -479,7 +479,7 @@

Library Stdlib.ZArith.BinIntDef

-

Bitwise functions

+

Bitwise functions

diff --git a/v9.0/stdlib/Stdlib.ZArith.Int.html b/v9.0/stdlib/Stdlib.ZArith.Int.html index 5593d00a71..4a5c6d9f3c 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Int.html +++ b/v9.0/stdlib/Stdlib.ZArith.Int.html @@ -48,7 +48,7 @@

Library Stdlib.ZArith.Int

-

An light axiomatization of integers (used in MSetAVL).

+

An light axiomatization of integers (used in MSetAVL).

@@ -73,7 +73,7 @@

Library Stdlib.ZArith.Int

-

A specification of integers

+

A specification of integers

@@ -209,7 +209,7 @@

Library Stdlib.ZArith.Int

-

Facts and tactics using Int

+

Facts and tactics using Int

@@ -563,7 +563,7 @@

Library Stdlib.ZArith.Int

-

An implementation of Int

+

An implementation of Int

diff --git a/v9.0/stdlib/Stdlib.ZArith.ZArith_dec.html b/v9.0/stdlib/Stdlib.ZArith.ZArith_dec.html index 4dbe8b24de..01786099a8 100644 --- a/v9.0/stdlib/Stdlib.ZArith.ZArith_dec.html +++ b/v9.0/stdlib/Stdlib.ZArith.ZArith_dec.html @@ -73,7 +73,7 @@

Library Stdlib.ZArith.ZArith_dec

-

Decidability of order on binary integers

+

Decidability of order on binary integers

@@ -115,7 +115,7 @@

Library Stdlib.ZArith.ZArith_dec

-

Cotransitivity of order on binary integers

+

Cotransitivity of order on binary integers

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zabs.html b/v9.0/stdlib/Stdlib.ZArith.Zabs.html index 8889b4cf85..0ba735874b 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zabs.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zabs.html @@ -73,7 +73,7 @@

Library Stdlib.ZArith.Zabs

-

Properties of absolute value

+

Properties of absolute value

@@ -91,7 +91,7 @@

Library Stdlib.ZArith.Zabs

-

Proving a property of the absolute value by cases

+

Proving a property of the absolute value by cases

@@ -116,7 +116,7 @@

Library Stdlib.ZArith.Zabs

-

Some results about the sign function.

+

Some results about the sign function.

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zbitwise.html b/v9.0/stdlib/Stdlib.ZArith.Zbitwise.html index 548165145e..ea87c6a8a0 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zbitwise.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zbitwise.html @@ -151,13 +151,13 @@

Library Stdlib.ZArith.Zbitwise

Explicit formulas for carry bits during addition. Conceptually, the theory -

here matches the bitblasting rules for integers. However, the vector of

+

here matches the bitblasting rules for integers. However, the vector of

-

carry bits is represented as a Z so it can be used in bitwise operations.

+

carry bits is represented as a Z so it can be used in bitwise operations.

-

The last three lemmas about addcarries are the main interface, but the

+

The last three lemmas about addcarries are the main interface, but the

-

generalization adccarries is provided as the same theory applies.

+

generalization adccarries is provided as the same theory applies.

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zbool.html b/v9.0/stdlib/Stdlib.ZArith.Zbool.html index 4cbbcfde37..2948b1ea22 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zbool.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zbool.html @@ -151,7 +151,7 @@

Library Stdlib.ZArith.Zbool

Properties of the deprecated Zeq_bool
-

Boolean operations from decidability of order

+

Boolean operations from decidability of order

The decidability of equality and order relations over type Z gives some boolean functions with the adequate specification.
@@ -183,7 +183,7 @@

Library Stdlib.ZArith.Zbool

-

Boolean comparisons of binary integers

+

Boolean comparisons of binary integers

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zcompare.html b/v9.0/stdlib/Stdlib.ZArith.Zcompare.html index bc23fe23de..bee743e411 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zcompare.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zcompare.html @@ -67,7 +67,7 @@

Library Stdlib.ZArith.Zcompare

-

Comparison on integers

+

Comparison on integers

@@ -82,7 +82,7 @@

Library Stdlib.ZArith.Zcompare

-

Transitivity of comparison

+

Transitivity of comparison

@@ -99,7 +99,7 @@

Library Stdlib.ZArith.Zcompare

-

Comparison and opposite

+

Comparison and opposite

@@ -111,7 +111,7 @@

Library Stdlib.ZArith.Zcompare

-

Comparison first-order specification

+

Comparison first-order specification

@@ -123,7 +123,7 @@

Library Stdlib.ZArith.Zcompare

-

Comparison and addition

+

Comparison and addition

@@ -145,7 +145,7 @@

Library Stdlib.ZArith.Zcompare

-

Successor and comparison

+

Successor and comparison

@@ -157,7 +157,7 @@

Library Stdlib.ZArith.Zcompare

-

Multiplication and comparison

+

Multiplication and comparison

@@ -178,7 +178,7 @@

Library Stdlib.ZArith.Zcompare

-

Relating x ?= y to =, <=, <, >= or >

+

Relating x ?= y to =, <=, <, >= or >

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zdiv.html b/v9.0/stdlib/Stdlib.ZArith.Zdiv.html index 9eb9dedfba..bcbcd2897f 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zdiv.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zdiv.html @@ -48,7 +48,7 @@

Library Stdlib.ZArith.Zdiv

-

Euclidean Division

+

Euclidean Division

@@ -88,7 +88,7 @@

Library Stdlib.ZArith.Zdiv

-

Main division theorems

+

Main division theorems

@@ -237,7 +237,7 @@

Library Stdlib.ZArith.Zdiv

-

Basic values of divisions and modulo.

+

Basic values of divisions and modulo.

@@ -293,7 +293,7 @@

Library Stdlib.ZArith.Zdiv

-

Order results about Z.modulo and Z.div

+

Order results about Z.modulo and Z.div

@@ -451,7 +451,7 @@

Library Stdlib.ZArith.Zdiv

-

Relations between usual operations and Z.modulo and Z.div

+

Relations between usual operations and Z.modulo and Z.div

@@ -690,7 +690,7 @@

Library Stdlib.ZArith.Zdiv

-

Compatibility

+

Compatibility

@@ -726,7 +726,7 @@

Library Stdlib.ZArith.Zdiv

-

A direct way to compute Z.modulo

+

A direct way to compute Z.modulo

@@ -778,9 +778,9 @@

Library Stdlib.ZArith.Zdiv

Another convention is possible for division by negative numbers: -

quotient is always the biggest integer smaller than or equal to a/b

+

quotient is always the biggest integer smaller than or equal to a/b

-

remainder is hence always positive or null.

+

remainder is hence always positive or null.

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zeuclid.html b/v9.0/stdlib/Stdlib.ZArith.Zeuclid.html index 00baac7e9a..ddb18057b9 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zeuclid.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zeuclid.html @@ -62,7 +62,7 @@

Library Stdlib.ZArith.Zeuclid

-

Definitions of division for binary integers, Euclid convention.

+

Definitions of division for binary integers, Euclid convention.

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zeven.html b/v9.0/stdlib/Stdlib.ZArith.Zeven.html index 31714468cd..238e591834 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zeven.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zeven.html @@ -175,7 +175,7 @@

Library Stdlib.ZArith.Zeven

-

Definition of Z.quot2, Z.div2 and properties wrt Zeven

+

Definition of Z.quot2, Z.div2 and properties wrt Zeven

and Zodd
diff --git a/v9.0/stdlib/Stdlib.ZArith.Zgcd_alt.html b/v9.0/stdlib/Stdlib.ZArith.Zgcd_alt.html index d89f9faab3..24cb2de14b 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zgcd_alt.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zgcd_alt.html @@ -48,7 +48,7 @@

Library Stdlib.ZArith.Zgcd_alt

-

Zgcd_alt : an alternate version of Z.gcd, based on Euclid's algorithm

+

Zgcd_alt : an alternate version of Z.gcd, based on Euclid's algorithm

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zhints.html b/v9.0/stdlib/Stdlib.ZArith.Zhints.html index 0d640d8083..c945802113 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zhints.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zhints.html @@ -101,7 +101,7 @@

Library Stdlib.ZArith.Zhints

-

Simplification lemmas

+

Simplification lemmas

@@ -115,7 +115,7 @@

Library Stdlib.ZArith.Zhints

  
-

Reversible simplification lemmas (no loss of information)

+

Reversible simplification lemmas (no loss of information)

Should clearly be declared as hints
@@ -170,7 +170,7 @@

Library Stdlib.ZArith.Zhints

  
-

Irreversible simplification lemmas

+

Irreversible simplification lemmas

Probably to be declared as hints, when no other simplification is possible
diff --git a/v9.0/stdlib/Stdlib.ZArith.Znat.html b/v9.0/stdlib/Stdlib.ZArith.Znat.html index 432a75b380..537e633a75 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Znat.html +++ b/v9.0/stdlib/Stdlib.ZArith.Znat.html @@ -94,7 +94,7 @@

Library Stdlib.ZArith.Znat

-

Chains of conversions

+

Chains of conversions

@@ -147,7 +147,7 @@

Library Stdlib.ZArith.Znat

-

Conversions between Z and N

+

Conversions between Z and N

@@ -551,7 +551,7 @@

Library Stdlib.ZArith.Znat

-

Conversions between Z and nat

+

Conversions between Z and nat

diff --git a/v9.0/stdlib/Stdlib.ZArith.Znumtheory.html b/v9.0/stdlib/Stdlib.ZArith.Znumtheory.html index c274f48f44..a001d52dfb 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Znumtheory.html +++ b/v9.0/stdlib/Stdlib.ZArith.Znumtheory.html @@ -244,7 +244,7 @@

Library Stdlib.ZArith.Znumtheory

-

Greatest common divisor (gcd).

+

Greatest common divisor (gcd).

@@ -306,7 +306,7 @@

Library Stdlib.ZArith.Znumtheory

-

Extended Euclid algorithm.

+

Extended Euclid algorithm.

@@ -394,7 +394,7 @@

Library Stdlib.ZArith.Znumtheory

-

Bezout's coefficients

+

Bezout's coefficients

@@ -430,7 +430,7 @@

Library Stdlib.ZArith.Znumtheory

-

Relative primality

+

Relative primality

@@ -524,7 +524,7 @@

Library Stdlib.ZArith.Znumtheory

-

Primality

+

Primality

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zorder.html b/v9.0/stdlib/Stdlib.ZArith.Zorder.html index e1cbf4b2e1..6422b4fcaa 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zorder.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zorder.html @@ -70,7 +70,7 @@

Library Stdlib.ZArith.Zorder

Properties of the order relations on binary integers
-

Trichotomy

+

Trichotomy

@@ -85,7 +85,7 @@

Library Stdlib.ZArith.Zorder

-

Decidability of equality and order on Z

+

Decidability of equality and order on Z

@@ -111,7 +111,7 @@

Library Stdlib.ZArith.Zorder

-

Relating strict and large orders

+

Relating strict and large orders

@@ -151,7 +151,7 @@

Library Stdlib.ZArith.Zorder

-

Equivalence and order properties

+

Equivalence and order properties

@@ -275,11 +275,11 @@

Library Stdlib.ZArith.Zorder

-

Compatibility of order and operations on Z

+

Compatibility of order and operations on Z

-

Successor

+

Successor

@@ -457,7 +457,7 @@

Library Stdlib.ZArith.Zorder

-

Addition

+

Addition

Compatibility of addition wrt to order
@@ -527,7 +527,7 @@

Library Stdlib.ZArith.Zorder

-

Multiplication

+

Multiplication

Compatibility of multiplication by a positive wrt to order
@@ -655,7 +655,7 @@

Library Stdlib.ZArith.Zorder

-

Square

+

Square

Simplification of square wrt order
@@ -670,7 +670,7 @@

Library Stdlib.ZArith.Zorder

-

Equivalence between inequalities

+

Equivalence between inequalities

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zpow_def.html b/v9.0/stdlib/Stdlib.ZArith.Zpow_def.html index 66ae502d0f..ec3a49ef61 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zpow_def.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zpow_def.html @@ -52,7 +52,7 @@

Library Stdlib.ZArith.Zpow_def

-

Power functions over Z

+

Power functions over Z

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zpow_facts.html b/v9.0/stdlib/Stdlib.ZArith.Zpow_facts.html index 4ac3058c13..b3b2c8dc1c 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zpow_facts.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zpow_facts.html @@ -131,7 +131,7 @@

Library Stdlib.ZArith.Zpow_facts

-

Z.pow and modulo

+

Z.pow and modulo

@@ -207,7 +207,7 @@

Library Stdlib.ZArith.Zpow_facts

-

Z.square: a direct definition of z^2

+

Z.square: a direct definition of z^2

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zpower.html b/v9.0/stdlib/Stdlib.ZArith.Zpower.html index ef850326f3..2c2b85189c 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zpower.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zpower.html @@ -53,7 +53,7 @@

Library Stdlib.ZArith.Zpower

-

Power functions over Z

+

Power functions over Z

@@ -153,7 +153,7 @@

Library Stdlib.ZArith.Zpower

-

Powers of 2

+

Powers of 2

@@ -282,7 +282,7 @@

Library Stdlib.ZArith.Zpower

-

Division by a power of two.

+

Division by a power of two.

diff --git a/v9.0/stdlib/Stdlib.ZArith.Zquot.html b/v9.0/stdlib/Stdlib.ZArith.Zquot.html index 3430e75ccd..311596b268 100644 --- a/v9.0/stdlib/Stdlib.ZArith.Zquot.html +++ b/v9.0/stdlib/Stdlib.ZArith.Zquot.html @@ -153,7 +153,7 @@

Library Stdlib.ZArith.Zquot

-

Division and Opposite

+

Division and Opposite

@@ -232,7 +232,7 @@

Library Stdlib.ZArith.Zquot

-

Unicity results

+

Unicity results

@@ -265,7 +265,7 @@

Library Stdlib.ZArith.Zquot

-

Order results about Zrem and Zquot

+

Order results about Zrem and Zquot

@@ -363,7 +363,7 @@

Library Stdlib.ZArith.Zquot

-

Relations between usual operations and Z.modulo and Z.div

+

Relations between usual operations and Z.modulo and Z.div

@@ -527,7 +527,7 @@

Library Stdlib.ZArith.Zquot

-

Interaction with "historic" Zdiv

+

Interaction with "historic" Zdiv

diff --git a/v9.0/stdlib/Stdlib.ZArith.auxiliary.html b/v9.0/stdlib/Stdlib.ZArith.auxiliary.html index e72f386993..dc8ca0e5b5 100644 --- a/v9.0/stdlib/Stdlib.ZArith.auxiliary.html +++ b/v9.0/stdlib/Stdlib.ZArith.auxiliary.html @@ -67,7 +67,7 @@

Library Stdlib.ZArith.auxiliary

-

Moving terms from one side to the other of an inequality

+

Moving terms from one side to the other of an inequality

diff --git a/v9.0/stdlib/Stdlib.btauto.Algebra.html b/v9.0/stdlib/Stdlib.btauto.Algebra.html index 2c3bfb5a78..d1335346a1 100644 --- a/v9.0/stdlib/Stdlib.btauto.Algebra.html +++ b/v9.0/stdlib/Stdlib.btauto.Algebra.html @@ -143,7 +143,7 @@

Library Stdlib.btauto.Algebra

-

Global, inductive definitions.

+

Global, inductive definitions.

@@ -216,7 +216,7 @@

Library Stdlib.btauto.Algebra

-

The core reflexive part.

+

The core reflexive part.

diff --git a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInt.html b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInt.html index 48ffb9a249..67c669cb7b 100644 --- a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInt.html +++ b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInt.html @@ -61,11 +61,11 @@

Library Stdlib.extraction.ExtrHaskellNatInt

-

Disclaimer: trying to obtain efficient certified programs

+

Disclaimer: trying to obtain efficient certified programs

-

by extracting nat into Int is definitively *not* a good idea.

+

by extracting nat into Int is definitively *not* a good idea.

-

See comments in ExtrOcamlNatInt.v.

+

See comments in ExtrOcamlNatInt.v.

diff --git a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInteger.html b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInteger.html index 9eea317f7e..b552e42281 100644 --- a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInteger.html +++ b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatInteger.html @@ -61,11 +61,11 @@

Library Stdlib.extraction.ExtrHaskellNatInteger

-

Disclaimer: trying to obtain efficient certified programs

+

Disclaimer: trying to obtain efficient certified programs

-

by extracting nat into Integer isn't necessarily a good idea.

+

by extracting nat into Integer isn't necessarily a good idea.

-

See comments in ExtrOcamlNatInt.v.

+

See comments in ExtrOcamlNatInt.v.

diff --git a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatNum.html b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatNum.html index e1deabdb85..cbe1e33eec 100644 --- a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatNum.html +++ b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellNatNum.html @@ -46,15 +46,15 @@

Library Stdlib.extraction.ExtrHaskellNatNum

-

Efficient (but uncertified) extraction of usual nat functions

+

Efficient (but uncertified) extraction of usual nat functions

-

into equivalent versions in Haskell's Prelude that are defined

+

into equivalent versions in Haskell's Prelude that are defined

-

for any Num typeclass instances. Useful in combination with

+

for any Num typeclass instances. Useful in combination with

-

Extract Inductive nat that maps nat onto a Haskell type that

+

Extract Inductive nat that maps nat onto a Haskell type that

-

implements Num.

+

implements Num.

diff --git a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellString.html b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellString.html index 5436597d08..cea7818ee7 100644 --- a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellString.html +++ b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellString.html @@ -46,7 +46,7 @@

Library Stdlib.extraction.ExtrHaskellString

-

Special handling of ascii and strings for extraction to Haskell.

+

Special handling of ascii and strings for extraction to Haskell.

@@ -67,16 +67,16 @@

Library Stdlib.extraction.ExtrHaskellString

-

At the moment, Coq's extraction has no way to add extra import

+

At the moment, Coq's extraction has no way to add extra import

-

statements to the extracted Haskell code. You will have to

+

statements to the extracted Haskell code. You will have to

-

manually add:

+

manually add:

* -

import qualified Data.Bits

+

import qualified Data.Bits

-

import qualified Data.Char

+

import qualified Data.Char

diff --git a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZInt.html b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZInt.html index 529a216e72..27dfc2f349 100644 --- a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZInt.html +++ b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZInt.html @@ -61,11 +61,11 @@

Library Stdlib.extraction.ExtrHaskellZInt

-

Disclaimer: trying to obtain efficient certified programs

+

Disclaimer: trying to obtain efficient certified programs

-

by extracting Z into Int is definitively *not* a good idea.

+

by extracting Z into Int is definitively *not* a good idea.

-

See comments in ExtrOcamlNatInt.v.

+

See comments in ExtrOcamlNatInt.v.

diff --git a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZNum.html b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZNum.html index 2e65eb8449..094b6c1860 100644 --- a/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZNum.html +++ b/v9.0/stdlib/Stdlib.extraction.ExtrHaskellZNum.html @@ -46,15 +46,15 @@

Library Stdlib.extraction.ExtrHaskellZNum

-

Efficient (but uncertified) extraction of usual Z functions

+

Efficient (but uncertified) extraction of usual Z functions

-

into equivalent versions in Haskell's Prelude that are defined

+

into equivalent versions in Haskell's Prelude that are defined

-

for any Num typeclass instances. Useful in combination with

+

for any Num typeclass instances. Useful in combination with

-

Extract Inductive Z that maps Z onto a Haskell type that

+

Extract Inductive Z that maps Z onto a Haskell type that

-

implements Num.

+

implements Num.

diff --git a/v9.0/stdlib/Stdlib.omega.PreOmega.html b/v9.0/stdlib/Stdlib.omega.PreOmega.html index f177aac16c..b97edd0af6 100644 --- a/v9.0/stdlib/Stdlib.omega.PreOmega.html +++ b/v9.0/stdlib/Stdlib.omega.PreOmega.html @@ -54,7 +54,7 @@

Library Stdlib.omega.PreOmega

-

Z.div_mod_to_equations, Z.quot_rem_to_equations, Z.to_euclidean_division_equations:

+

Z.div_mod_to_equations, Z.quot_rem_to_equations, Z.to_euclidean_division_equations:

the tactics for preprocessing Z.div and Z.modulo, Z.quot and Z.rem
diff --git a/v9.0/stdlib/index_global_T.html b/v9.0/stdlib/index_global_T.html index 060d357a3e..11f2797e0a 100644 --- a/v9.0/stdlib/index_global_T.html +++ b/v9.0/stdlib/index_global_T.html @@ -527,8 +527,8 @@ t [abbreviation, in Stdlib.micromega.VarMap]
t [inductive, in Stdlib.micromega.VarMap]
t [inductive, in Stdlib.Vectors.Fin]
-Tactics [library]
Tactics [library]
+Tactics [library]
Tadd [definition, in Stdlib.rtauto.Bintree]
tail [abbreviation, in Stdlib.Lists.List]
tail [definition, in Stdlib.micromega.Env]
@@ -576,8 +576,8 @@ tan_PI [lemma, in Stdlib.Reals.Rtrigo_calc]
target [projection, in Stdlib.micromega.ZifyClasses]
target_prop [projection, in Stdlib.micromega.ZifyClasses]
-Tauto [library]
Tauto [library]
+Tauto [library]
tauto_checker_sound [lemma, in Stdlib.micromega.Tauto]
tauto_checker [definition, in Stdlib.micromega.Tauto]
TBOp [projection, in Stdlib.micromega.ZifyClasses]
diff --git a/v9.0/stdlib/index_global_W.html b/v9.0/stdlib/index_global_W.html index 71aad0a586..111fa3ed0a 100644 --- a/v9.0/stdlib/index_global_W.html +++ b/v9.0/stdlib/index_global_W.html @@ -928,8 +928,8 @@ WEqProperties_fun.Add [definition, in Stdlib.FSets.FSetEqProperties]
WEqProperties_fun.MP [module, in Stdlib.FSets.FSetEqProperties]
WEqProperties_fun [module, in Stdlib.FSets.FSetEqProperties]
-Wf [library]
Wf [library]
+Wf [library]
WFacts [module, in Stdlib.MSets.MSetFacts]
WFacts [module, in Stdlib.FSets.FMapFacts]
WFacts [module, in Stdlib.FSets.FSetFacts]
diff --git a/v9.0/stdlib/index_library_T.html b/v9.0/stdlib/index_library_T.html index b65df66395..9009a427af 100644 --- a/v9.0/stdlib/index_library_T.html +++ b/v9.0/stdlib/index_library_T.html @@ -523,10 +523,10 @@

T (library)

-Tactics
Tactics
-Tauto
+Tactics
Tauto
+Tauto
Transitive_Closure