50 search results for "tag:"keyword:C""

Showing 1 - 50
  1. coq-algorand

    No documentation

    A verified model of the Algorand consensus protocol in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:distributed algorithms keyword:blockchain keyword:consensus keyword:algorand logpath:Algorand date:2022-11-20
    Musab A. Alturki Jing Chen Victor Luchangco Brandon Moore Karl Palmskog et al.
    1.4
    NCSA
    Used by 0 other packages
    21 Nov 2022
  2. coq-approx-models

    No documentation

    Rigorous approximations with a posteriori verified operations
    category:Mathematics/Approximation Theory keyword:approximation theory keyword:Chebyshev polynomials keyword:certificate-based approximation logpath:ApproxModels date:2021-06-15
    Florent Bréhard Assia Mahboubi Damien Pous
    1.0
    CECILL-B
    Used by 0 other packages
    16 Jun 2021
  3. coq-chapar

    No documentation

    A framework for verification of causal consistency for distributed key-value stores and their clients in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:causal consistency keyword:key-value stores keyword:distributed algorithms keyword:program verification logpath:Chapar date:2023-12-28
    Mohsen Lesani Christian J. Bell Adam Chlipala
    8.17.0
    MIT
    Used by 0 other packages
    28 Dec 2023
  4. coq-coinduction

    No documentation

    A library for doing proofs by (enhanced) coinduction
    keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity logpath:Coinduction date:2024-09-18
    Damien Pous
    1.20
    LGPL-3.0-or-later
    Used by 1 other packages
    18 Sep 2024
  5. coq-coinduction-examples

    No documentation

    Examples on how to use the coq-coinduction library, for doing proofs by (enhanced) coinduction
    keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity keyword:divergence keyword:streams keyword:CCS logpath:CoinductionExamples
    Damien Pous
    1.7
    LGPL-3.0-or-later
    Used by 0 other packages
    13 Jul 2023
  6. coq-color

    No documentation

    A library on rewriting theory and termination
    date:2023-06-28 logpath:CoLoR category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Data Types and Data Structures category:Computer Science/Lambda Calculi category:Mathematics/Algebra category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Type theory category:Miscellaneous/Extracted Programs/Type checking unification and normalization keyword:rewriting keyword:termination keyword:lambda calculus keyword:list keyword:multiset keyword:polynomial keyword:vectors keyword:matrices keyword:FSet keyword:FMap keyword:term keyword:context keyword:substitution keyword:universal algebra keyword:varyadic term keyword:string keyword:alpha-equivalence keyword:de Bruijn indices keyword:simple types keyword:matching keyword:unification keyword:relation keyword:ordering keyword:quasi-ordering keyword:lexicographic ordering keyword:ring keyword:semiring keyword:well-foundedness keyword:noetherian keyword:finitely branching keyword:dependent choice keyword:infinite sequences keyword:non-termination keyword:loop keyword:graph keyword:path keyword:transitive closure keyword:strongly connected components keyword:topological ordering keyword:rpo keyword:horpo keyword:dependency pair keyword:dependency graph keyword:semantic labeling keyword:reducibility keyword:Girard keyword:fixpoint theorem keyword:Tarski keyword:pigeon-hole principle keyword:Ramsey theorem
    Frédéric Blanqui Adam Koprowski Sébastien Hinderer Pierre-Yves Strub Sidi Ould Biha et al.
    1.8.5
    CeCILL-2.1
    Used by 0 other packages
    16 Apr 2024
  7. coq-comp-dec-modal

    No documentation

    Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse
    category:Mathematics/Logic/Modal logic keyword:modal logic keyword:completeness keyword:decidability keyword:Hilbert system keyword:computation tree logic keyword:propositional dynamic logic logpath:CompDecModal date:2024-07-24
    Christian Doczkal
    1.2
    CECILL-B
    Used by 0 other packages
    24 Jul 2024
  8. coq-compcert

    No documentation

    The CompCert C compiler (64 bit)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert date:2024-05-02
    Xavier Leroy
    3.14
    INRIA Non-Commercial License Agreement
    Used by 3 other packages
    08 May 2024
  9. coq-compcert-32

    No documentation

    The CompCert C compiler (32 bit)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert32 date:2023-07-04
    Xavier Leroy
    3.13.1
    INRIA Non-Commercial License Agreement
    Used by 1 other packages
    09 Nov 2023
  10. coq-compcert-64

    No documentation

    The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert64 date:2020-04-29
    Xavier Leroy
    3.7+8.12~coq_platform
    INRIA Non-Commercial License Agreement
    Used by 1 other packages
    28 Jul 2020
  11. coq-coqtail

    No documentation

    Library of mathematical theorems and tools proved inside the Coq
    category:Mathematics/Real Calculus and Topology keyword:real analysis keyword:complex analysis date:2024-07-13 logpath:Coqtail
    Guillaume Allais Sylvain Dailler Hugo Férée Jean-Marie Madiot Pierre-Marie Pédrot et al.
    8.20
    LGPL-3.0-only
    Used by 0 other packages
    14 Jul 2024
  12. coq-corn

    No documentation

    The Coq Constructive Repository at Nijmegen
    category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology category:Mathematics/Exact Real computation keyword:constructive mathematics keyword:algebra keyword:real calculus keyword:real numbers keyword:Fundamental Theorem of Algebra logpath:CoRN date:2024-04-23
    Evgeny Makarov Robbert Krebbers Eelis van der Weegen Bas Spitters Jelle Herold et al.
    8.19.0
    GPL-2.0
    Used by 0 other packages
    23 Apr 2024
  13. coq-fcsl-pcm

    No documentation

    Coq library of Partial Commutative Monoids
    category:Computer Science/Data Types and Data Structures keyword:partial commutative monoids keyword:separation logic keyword:concurrency logpath:pcm
    Aleksandar Nanevski Anton Trunov Alexander Gryzlov
    2.0.0
    Apache-2.0
    Used by 4 other packages
    18 Sep 2024
  14. coq-formalv-time

    No documentation

    A Coq library for time and date arithmetic according to the UTC standard with leap seconds
    keyword:time keyword:date keyword:timestamp keyword:coq formalization logpath:formalv
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.2.0
    PolyForm Noncommercial License 1.0.0
    Used by 0 other packages
    24 Jul 2023
  15. coq-freesim

    No documentation

    Stuttering For Free
    keyword:simulation keyword:coinduction keyword:dual non-determinism keyword:up to techniques keyword:companion keyword:Interaction Trees keyword:CompCert logpath:FreeSim
    Minki Cho, Youngju Song, Dongjae Lee
    1.0.0
    BSD-3-Clause
    Used by 0 other packages
    19 Sep 2023
  16. coq-gaia-ordinals

    No documentation

    Implementation and properties of ordinals in Coq using Mathematical Components
    category:Mathematics/Logic/Set theory category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordered sets keyword:ordinal arithmetic keyword:ordinal numbers keyword:cardinal numbers logpath:gaia.ordinals date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 1 other packages
    11 Aug 2024
  17. coq-geocoq

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:Hilbert keyword:Euclid keyword:Elements keyword:Pappus keyword:Desargues keyword:arithmetization keyword:Pythagoras keyword:Thales' intercept theorem keyword:continuity keyword:ruler and compass keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space keyword:automation date:2024-03-24
    Michael Beeson <profbeeson@gmail.com> Gabriel Braun <gabriel.braun@unistra.fr> Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Charly Gries <charly.gries@etu.unistra.fr> et al.
    2.5.0
    LGPL-3.0-only
    Used by 0 other packages
    25 Mar 2024
  18. coq-geocoq-algebraic

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space date:2024-03-24
    Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Stéphane Kastenbaum <stephane.kastenbaum@gmail.com>
    2.5.0
    LGPL-3.0-only
    Used by 2 other packages
    25 Mar 2024
  19. coq-geocoq-main

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:foundations keyword:Tarski keyword:Hilbert keyword:Euclid keyword:Pappus keyword:Desargues keyword:arithmetization keyword:Pythagoras keyword:Thales' intercept theorem keyword:continuity keyword:ruler and compass keyword:parallel postulates date:2024-03-24
    Gabriel Braun <gabriel.braun@unistra.fr> Pierre Boutry <contact@pierre.boutry.fr> Charly Gries <charly.gries@etu.unistra.fr> Julien Narboux <narboux@unistra.fr> Pascal Schreck <schreck@unistra.fr>
    2.5.0
    LGPL-3.0-only
    Used by 1 other packages
    25 Mar 2024
  20. coq-geocoq-pof

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space date:2024-03-24
    Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Stéphane Kastenbaum <stephane.kastenbaum@gmail.com>
    2.5.0
    LGPL-3.0-only
    Used by 0 other packages
    25 Mar 2024
  21. coq-giskard

    No documentation

    Verified model of the Giskard consensus protocol in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:Giskard keyword:consensus keyword:blockchain logpath:Giskard date:2022-11-23
    Elaine Li Karl Palmskog Mircea Sebe
    1.1
    NCSA
    Used by 0 other packages
    21 Jun 2023
  22. coq-http

    No documentation

    HTTP in Coq
    category:Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols category:Miscellaneous/Extracted Programs/Decision procedures keyword:co-induction keyword:extraction keyword:reactive systems logpath:HTTP
    Yishuai Li <yishuai@cis.upenn.edu> Li-yao Xia <xialiyao@cis.upenn.edu> Yao Li <liyao@cis.upenn.edu> Azzam Althagafi <aazzam@cis.upenn.edu> Benjamin C. Pierce <bcpierce@cis.upenn.edu>
    0.2.1
    MPL-2.0
    Used by 0 other packages
    20 Jul 2023
  23. coq-huffman

    No documentation

    Coq proof of the correctness of the Huffman coding algorithm
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Miscellaneous/Extracted Programs/Combinatorics keyword:data compression keyword:code keyword:huffman tree logpath:Huffman date:2023-07-09
    Laurent Théry
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    01 Aug 2023
  24. coq-infotheo

    No documentation

    Discrete probabilities and information theory for Coq
    keyword:information theory keyword:probability keyword:error-correcting codes keyword:convexity logpath:infotheo date:2024-12-20
    Reynald Affeldt, AIST Manabu Hagiwara, Chiba U. (previously AIST) Jonas Senizergues, ENS Cachan (internship at AIST) Jacques Garrigue Kazuhiko Sakaguchi, Tsukuba U. et al.
    0.7.7
    LGPL-2.1-or-later
    Used by 1 other packages
    19 Dec 2024
  25. coq-jsast

    No documentation

    A minimal JavaScript syntax tree carved out of the JsCert project
    keyword:javascript keyword:compiler date:2020-07-29 logpath:JsAst
    Martin Bodin <> Arthur Charguéraud <> Daniele Filaretti <> Philippa Gardner <> Sergio Maffeis <> et al.
    3.0.0
    BSD-2-Clause
    Used by 1 other packages
    26 May 2022
  26. coq-lemma-overloading

    No documentation

    Libraries demonstrating design patterns for programming and proving with canonical structures in Coq
    category:Computer Science/Data Types and Data Structures keyword:canonical structures keyword:proof automation keyword:Hoare type theory keyword:lemma overloading logpath:LemmaOverloading date:2020-08-12
    Georges Gonthier Beta Ziliani Aleksandar Nanevski Derek Dreyer
    8.12.0
    GPL-3.0-or-later
    Used by 0 other packages
    13 Aug 2020
  27. coq-libvalidsdp

    No documentation

    LibValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:libValidSDP category:Miscellaneous/Coq Extensions logpath:libValidSDP
    Pierre Roux <pierre.roux@onera.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr>
    1.0.2
    LGPL-2.1-or-later
    Used by 1 other packages
    13 Dec 2023
  28. coq-mathcomp-algebra

    No documentation

    Mathematical Components Library on Algebra
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:algebraic structure hierarchies keyword:archimedean field keyword:floor keyword:ceil keyword:intervals keyword:matrices keyword:vectors keyword:block matrices keyword:determinant keyword:Cramer rule keyword:Vandermonde matrices keyword:LUP decomposition keyword:Gaussian elimination keyword:matrix rank keyword:eigen values keyword:single variable polynomials keyword:bivariate polynomials keyword:polynomial division keyword:integers keyword:rational numbers keyword:semirings keyword:rings keyword:left algebra keyword:left module keyword:unit rings keyword:field keyword:algebraically closed field keyword:additive morphisms keyword:ring morphisms keyword:finite dimensional vector spaces keyword:complex numbers keyword:square root logpath:mathcomp.algebra
    The Mathematical Components team
    2.3.0
    CECILL-B
    Used by 29 other packages
    29 Nov 2024
  29. coq-mathcomp-analysis

    No documentation

    An analysis library for mathematical components
    category:Mathematics/Real Calculus and Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Landau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.8.0
    CECILL-C
    Used by 7 other packages
    19 Dec 2024
  30. coq-mathcomp-apery

    No documentation

    A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:apery recurrence keyword:irrationality keyword:creative telescoping logpath:mathcomp.apery date:2022-05-05
    Frédéric Chyzak Assia Mahboubi Thomas Sibut-Pinote
    1.0.2
    CECILL-C
    Used by 0 other packages
    05 May 2022
  31. coq-mathcomp-cad

    No documentation

    Formal Proof of Cylindrical Algebraic Decomposition
    keyword:CAD logpath:SemiAlgebraic
    Cyril Cohen Boris Djalal Quentin Vermande
    1.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Dec 2024
  32. coq-mathcomp-character

    No documentation

    Mathematical Components Library on character theory
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:character logpath:mathcomp.character
    The Mathematical Components team
    2.3.0
    CECILL-B
    Used by 1 other packages
    29 Nov 2024
  33. coq-mathcomp-classical

    No documentation

    A library for classical logic for mathematical components
    category:Mathematics/Logic/Classical logic keyword:classical logic keyword:logic keyword:sets keyword:set theory keyword:function keyword:cardinal keyword:filter logpath:mathcomp.classical
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.8.0
    CECILL-C
    Used by 2 other packages
    19 Dec 2024
  34. coq-mathcomp-dioid

    No documentation

    Dioid
    keyword:dioid keyword:semiring keyword:complete dioid category:Miscellaneous/Coq Extensions logpath:mathcomp.dioid
    Lucien Rakotomalala <lucien.rakotomalala@onera.fr> Pierre Roux <pierre.roux@onera.fr>
    0.2
    CECILL-B
    Used by 0 other packages
    20 Dec 2021
  35. coq-mi-cho-coq

    No documentation

    A specification of Michelson in Coq to prove properties about smart contracts in Tezos
    category:Computer Science/Programming Languages/Formal Definitions and Theory date:2021-06-15 keyword:cryptocurrency keyword:michelson keyword:semantics keyword:smart-contract keyword:tezos logpath:Michocoq logpath:Michocott
    Raphaël Cauderlier Bruno Bernardo Julien Tesson Arvid Jakobsson
    1.0.0
    MIT
    Used by 0 other packages
    21 Jun 2021
  36. coq-of-ocaml

    No documentation

    Compile a subset of OCaml to Coq
    date:2020-03-20 keyword:compilation keyword:OCaml logpath:OCaml
    Guillaume Claret
    2.1.0
    MIT
    Used by 0 other packages
    20 May 2020
  37. coq-paco

    No documentation

    Coq library implementing parameterized coinduction
    date:2024-10-09 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Mathematics/Logic keyword:co-induction keyword:simulation keyword:parameterized greatest fixed point logpath:Paco
    Chung-Kil Hur <gil.hur@sf.snu.ac.kr> Georg Neis <neis@mpi-sws.org> Derek Dreyer <dreyer@mpi-sws.org> Viktor Vafeiadis <viktor@mpi-sws.org> Minki Cho <minki.cho@sf.snu.ac.kr>
    4.2.1
    BSD-3-Clause
    Used by 3 other packages
    10 Oct 2024
  38. coq-qcert

    No documentation

    Verified compiler for data-centric languages
    keyword:databases keyword:queries keyword:relational keyword:compiler date:2020-08-22 logpath:Qcert
    Josh Auerbach <> Martin Hirzel <> Louis Mandel <> Avi Shinnar <> Jerome Simeon <>
    2.2.0
    Apache-2.0
    Used by 0 other packages
    22 May 2022
  39. coq-quantumlib

    No documentation

    Coq library for reasoning about quantum programs
    keyword:quantum keyword:qwire keyword:sqir keyword:matrices keyword:vectors keyword:linear algebra keyword:complex numbers category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology date:2024-05-27 logpath:QuantumLib
    inQWIRE
    1.5.1
    MIT
    Used by 0 other packages
    29 Jul 2024
  40. coq-ssprove

    No documentation

    A Foundational Framework for Modular Cryptographic Proofs
    keyword:cryptography logpath:SSProve
    SSProve team
    0.2.2
    MIT
    Used by 0 other packages
    28 Nov 2024
  41. coq-tlc

    No documentation

    TLC: A Library for Classical Coq
    category:Computer Science/Data Types and Data Structures date:2024-02-09 keyword:classical logic logpath:TLC
    Arthur Charguéraud
    20240209
    MIT
    Used by 2 other packages
    13 Feb 2024
  42. coq-validsdp

    No documentation

    ValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:ValidSDP
    Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr>
    1.0.2
    LGPL-2.1-or-later
    Used by 0 other packages
    13 Dec 2023
  43. coq-vlsm

    No documentation

    Coq formalization of validating labelled state transition and message production systems
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:consensus keyword:fault tolerance keyword:distributed algorithms keyword:Paxos logpath:VLSM date:2023-12-15
    Mihai Calancea Denisa Diaconescu Wojciech Kołowski Elaine Li Brandon Moore et al.
    1.3
    BSD-3-Clause
    Used by 0 other packages
    15 Dec 2023
  44. coq-void

    No documentation

    MathComp instances for the empty type (Empty_set)
    keyword:empty type keyword:class instances category:Computer Science/Data Types and Data Structures date:2019-10-08 logpath:void
    Arthur Azevedo de Amorim
    0.1.0
    MIT
    Used by 0 other packages
    08 Oct 2019
  45. coq-vst

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-04-12
    Andrew W. Appel Lennart Beringer William Mansky Josiah Dodds Qinxiang Cao et al.
    3.0beta2
    BSD-2-Clause
    Used by 0 other packages
    15 Apr 2024
  46. coq-vst-32

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-03-20
    Andrew W. Appel Lennart Beringer Josiah Dodds Qinxiang Cao Aquinas Hobor et al.
    2.14
    BSD-2-Clause
    Used by 0 other packages
    21 Mar 2024
  47. coq-vst-64

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2020-08-02
    Andrew W. Appel Lennart Beringer Sandrine Blazy Qinxiang Cao Santiago Cuellar et al.
    2.6
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    03 Aug 2020
  48. coq-vst-iris

    No documentation

    Verified Software Toolchain with Iris
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2023-01-24
    William Mansky Shengyi Wang
    2.11.1
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    25 Jan 2023
  49. coq-yalla

    No documentation

    Yalla library
    keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2024-09-16 logpath:Yalla
    Olivier Laurent
    2.0.6
    LGPL-3.0-or-later
    Used by 0 other packages
    16 Sep 2024
  50. coq-zorns-lemma

    No documentation

    This library develops some basic set theory in Coq
    category:Mathematics/Logic/Set theory date:2023-08-18 keyword:set theory keyword:cardinals keyword:ordinal numbers keyword:finite keyword:countable keyword:quotients keyword:well-orders keyword:Zorn's lemma logpath:ZornsLemma
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 1 other packages
    21 Aug 2023