aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
AgeCommit message (Collapse)Author
2020-09-16Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-namesJasper Hugunin
The bitwise tactic was performing `intros ?m`, and the name m got used later in many proofs. I defined a tactic notation `bitwise as m` to be able to provide the name for `m` explicitly. I did not make the notation local, because it seems like it would be useful for any clients using `bitwise` who want to avoid generated names. I have relatively little experience with writing Ltac and tactic notations, so if my solution can be improved, please show me how.
2020-09-16Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-namesJasper Hugunin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-08-25Modify Numbers/NatInt/NZGcd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZDiv.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZLog.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZPow.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZParity.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZOrder.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZMul.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZAdd.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Numbers/NatInt/NZBase.v to compile with -mangle-namesJasper Hugunin
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-09Bring Int63 notations into line with stdlibJason Gross
We also put them in a module, so users can `Require Int63. Import Int63.Int63Notations` without needing to unqualify the primitives. In particular, we change - `a \% m` into `a mod m` to correspond with the notation in ZArith - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere - `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation The old notations are still accessible as deprecated notations. Fixes #12454
2020-05-09Hexadecimal: conversion to/from Coq stringsPierre Roux
2020-05-09Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijectionsPierre Roux
2020-05-09Decimal: prove numeral notation for QPierre Roux
Fill in the proofs, adding a few neessary lemmas along the way.
2020-05-09Decimal: specify numeral notation for QPierre Roux
2020-05-09Uniformize indentation in theories/NumbersPierre Roux
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-05-04add order properties about boolOlivier Laurent
2020-04-19Fix a typoPierre Roux
2020-04-08Merge PR #11909: Make the level of ≡ in Int63 consistent with =Hugo Herbelin
Reviewed-by: anton-trunov
2020-03-25Make the level of ≡ in Int63 consistent with =Jason Gross
Fixes #11905
2020-03-24[stdlib] Do not rely on failing “auto”Vincent Laporte
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-02-26Consolidate int63-related notationsMaxime Dénès
We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
Ack-by: fajb Reviewed-by: ppedrot
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
This could be Prop (for compat with usual Coq), Set (for HoTT), or actually an arbitrary "i". Take lower bound of universes into account in pretyping/engine Reinstate proper elaboration of SProp <= l constraints: replacing is_small with equality with lbound is _not_ semantics preserving! lbound = Set Elaborate template polymorphic inductives with lower bound Prop This will make more constraints explicit Check univ constraints with Prop as lower bound for template inductives Restrict template polymorphic universes to those not bounded from below Fixes #9294 fix suggested by Matthieu Try second fix suggested by Matthieu Take care of modifying elaboration for record declarations as well. Rebase and export functions for debug Remove exported functions used while debugging Add a new typing flag "check_template" and option "-no-template-checl" This parameterizes the new criterion on template polymorphic inductives to allow bypassing it (necessary for backward compatibility). Update checker to the new typing flags structure Switch on the new template_check flag to allow old unsafe behavior in indTyping. This is the only change of code really impacting the kernel, together with the commit implementing unbounded from below and parameterization by the lower bound on universes. Add deprecated option `Unset Template Check` allowing to make proof scripts work with both 8.9 and 8.10 for a while Fix `Template Check` option name and test it Add `Unset Template Check` to Coq89.v Cooking of inductives and template-check tests Cleanup test-suite file for template check / universes(template) flags cookind tests Move test of `Unset Template Check` to the failure/ dir, but comment it for now Template test-suite test explanation Overlays for PR 9918 Overlay for paramcoq Add overlay for fiat_parsers (-no-template-check) Add overlay for fiat_crypto_legacy Update fiat-crypto legacy overlay Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made. Remove overlay that should no longer be necessary The setting in the compat file should handle it Remove now-merged fiat-crypto-legacy overlay Update `Print Assumptions` to reflect the typing flag for template checking Fix About and Print Assumptions for template poly, giving info on which variables are actually polymorphic Fix pretty printing to print global universe levels properly Fix printing of template polymorphic universes Fix pretty printing for template polymorphism on no universe Fix interaction of template check and universes(template) flag Fix indTyping to really check if there is any point in polymorphism: the conclusion sort should be parameterized over at least one local universe Indtyping fixes for template polymorphic Props Allow explicit template polymorphism again Adapt to new indTyping interface Handle the case of template-polymorphic on no universes correctly (morally Type0m univ represented as Prop). Fix check of meaningfullness of template polymorphism in the kernel. It is now done w.r.t the min_univ, the minimal universe inferred for the inductive/record type, independently of the user-written annotation which must only be larger than min_univ. This preserves compatibility with UniMath and template-polymorphism as it has been implemented up-to now. Comment on identity non-template-polymorphism Remove incorrect universes(template) attributes from ssr simpl_fun can be meaningfully template-poly, as well as pred_key (although the use is debatable: it could just as well be in Prop). Move `fun_of_simpl` coercion declaration out of section to respect uniform inheritance Remove incorrect uses of #[universes(template)] from the stdlib Extraction of micromega changes due to moving an ind decl out of a section Remove incorrect uses of #[universes(template)] from plugins Fix test-suite files, removing incorrect #[universes(template)] attributes Remove incorrect #[universes(template)] attributes in test-suite Fix test-suite Remove overlays as they have been merged upstream.
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes ↵Maxime Dénès
#10551). Reviewed-by: maximedenes Reviewed-by: proux01
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Add a non-overflow precondition to diveucl_21 to align it on standard ↵thery
implementations.
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-25[Int63] Remove redundant misnamed lemma lsr_add_distrVincent Laporte
This lemma is lsl_add_distr (about “<<” rather than “>>”). See lemmas bit_add_or and lor_lsr for related properties.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-20 17:28:38 +0000