aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/Peano/NPeano.v
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* More dynamic argument scopesGravatar letouzey2013-07-17
* Updating headers.Gravatar herbelin2012-08-08
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Annotations at functor applications:Gravatar letouzey2011-02-11
* Numbers: simplier spec for testbitGravatar letouzey2011-01-20
* NPeano.modulo : another trick a la "minus" for having a decreasing argGravatar letouzey2010-12-17
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* Nicer log2 function for nat (suggested by Hugo)Gravatar letouzey2010-12-17
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
* NZSqrt : since spec is complete, no need for morphism axiom sqrt_wdGravatar letouzey2010-11-02
* NZLog : since spec is complete, no need for morphism axiom log2_wdGravatar letouzey2010-11-02
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* NPeano: A log2 function for natGravatar letouzey2010-11-02
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
* Add sqrt in NumbersGravatar letouzey2010-10-19
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
* Avoid some more re-declarations of Equivalence instancesGravatar letouzey2010-01-14
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Numbers abstract layer: more Module Type, used especially for divisions.Gravatar letouzey2010-01-05
* A generic euclidean division in Numbers (Still Work-In-Progress)Gravatar letouzey2009-12-15
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* Numbers: more (syntactic) changes toward new style of type classesGravatar letouzey2009-11-06
* Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcGravatar letouzey2009-11-03
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-03
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-02
* switch theories/Numbers from Set to Type (both the abstract and the bignum pa...Gravatar letouzey2008-05-22
* Coq headers + $ in theories/Numbers filesGravatar letouzey2008-05-15
* Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...Gravatar emakarov2007-11-14
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* An update of theories/NumbersGravatar emakarov2007-11-03
* Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu...Gravatar emakarov2007-10-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 05:00:05 +0000