coq/theories/Arith, branch masterThe formal proof systemadd Cantor pairing to_nat and its inverse of_nat2021-04-02T15:24:12+00:00Andrej Dudenhefner2021-03-25T17:19:12+00:002b02934f003836133d194d29f6a32c289280263c
add polynomial specifications of to_nat
add changelog and doc entries
add polynomial specifications of to_nat
add changelog and doc entries
Explicitly annotate all hint declarations of the standard library.2020-11-16T11:28:27+00:00Pierre-Marie Pédrot2020-11-14T16:55:07+00:0068cd077344ce37db1a601079dbc4fdcae6c8d41f
By default Coq stdlib warnings raise an error, so this is really required.
By default Coq stdlib warnings raise an error, so this is really required.
Modify Arith/Euclid.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T22:56:26+00:006f1e74f0445eae57e81a84bdfadd5f1b1b37a637
Modify Arith/Div2.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T22:55:15+00:00b777146eca9ae9f4593dc3d110655c2241c409dc
Modify Arith/Even.v to compile with -mangle-names2020-10-12T02:05:14+00:00Jasper Hugunin2020-10-09T22:53:47+00:0017ba1c432409cd84a83f29a5014b3597cfae9b03
Modify Arith/Wf_nat.v to compile with -mangle-names2020-09-16T19:46:57+00:00Jasper Hugunin2020-09-13T00:23:54+00:0054228bf1af0af83f0b603b6d7707601d139663be
Modify Arith/EqNat.v to compile with -mangle-names2020-09-16T19:46:57+00:00Jasper Hugunin2020-09-13T00:15:52+00:00be0c955cd75be5968fe0fddb4556317cc7c713c9
Modify Arith/Factorial.v to compile with -mangle-names2020-09-16T19:46:57+00:00Jasper Hugunin2020-09-13T00:13:21+00:00c82bea6f76ad0b6ea57cda027cc49ec009850a48
Modify Arith/Compare_dec.v to compile with -mangle-names2020-09-16T19:46:57+00:00Jasper Hugunin2020-09-13T00:11:36+00:001a0017b8b85d2536d333f6b85f311aefa219b33a
Modify Arith/Peano_dec.v to compile with -mangle-names2020-09-16T19:46:57+00:00Jasper Hugunin2020-09-13T00:09:44+00:000f6f3eedb65c3b061b4d4443c18e57ad38bb1f41