569 search results for ""

Showing 501 - 550
  1. rocq-hollight-logic

    No documentation

    HOL-Light library necessary for translating unify
    logpath:HOLLight_Logic date:2025-10-21 keyword:HOL-Light keyword:first order logic
    Antoine Gontard
    0.0.0
    CeCILL-2.1
    Used by 0 other packages
    25 Oct 2025
  2. rocq-hollight-logic-unif

    No documentation

    HOL-Light library necessary for translating unify
    logpath:HOLLight_Logic_fole date:2025-10-16 keyword:HOL-Light keyword:first order logic
    Antoine Gontard
    0.0.0
    CeCILL-2.1
    Used by 1 other packages
    22 Oct 2025
  3. rocq-iris

    No documentation

    A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
    date:2026-03-05 logpath:iris.prelude logpath:iris.algebra logpath:iris.si_logic logpath:iris.bi logpath:iris.proofmode logpath:iris.base_logic logpath:iris.program_logic
    The Iris Team
    4.5.0
    BSD-3-Clause
    Used by 1 other packages
    06 Mar 2026
  4. rocq-iris-heap-lang

    No documentation

    The canonical example language for Iris
    date:2026-03-05 logpath:iris.heap_lang
    The Iris Team
    4.5.0
    BSD-3-Clause
    Used by 0 other packages
    06 Mar 2026
  5. rocq-jsast

    No documentation

    A minimal JavaScript syntax tree carved out of the JsCert project
    keyword:javascript keyword:compiler date:2026-02-27 logpath:JsAst
    Martin Bodin <> Arthur Charguéraud <> Daniele Filaretti <> Philippa Gardner <> Sergio Maffeis <> et al.
    4.0.0
    BSD-2-Clause
    Used by 0 other packages
    02 Mar 2026
  6. rocq-lean-import

    No documentation

    Plugin allowing Rocq to import Lean exported files
    logpath:LeanImport
    Gaëtan Gilbert
    0.0.1
    LGPL-2.1-only
    Used by 0 other packages
    10 Dec 2025
  7. rocq-libhyps

    No documentation

    Hypotheses manipulation library
    keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming category:Miscellaneous/Coq Extensions logpath:LibHyps date:2026-04-13
    Pierre Courtieu
    5.0
    MIT
    Used by 0 other packages
    17 Apr 2026
  8. rocq-listz

    No documentation

    A Rocq library of lists with indices in Z
    date:2026-04-17 logpath:listz
    François Pottier <francois.pottier@inria.fr>
    20260417
    LGPL-2.1-only
    Used by 1 other packages
    17 Apr 2026
  9. rocq-marble

    No documentation

    Data structures based on machine integers and primitive arrays
    date:2026-04-21 logpath:marble
    François Pottier <francois.pottier@inria.fr>
    20260421
    LGPL-2.1-only
    Used by 0 other packages
    22 Apr 2026
  10. rocq-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.5.0
    CECILL-B
    Used by 8 other packages
    13 Nov 2025
  11. rocq-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.16.0
    CECILL-C
    Used by 2 other packages
    16 Mar 2026
  12. rocq-mathcomp-analysis-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers category:Mathematics/Real Calculus and Topology keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 1 other packages
    16 Mar 2026
  13. rocq-mathcomp-bigenough

    No documentation

    A small library to do epsilon - N reasoning
    keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenough
    Cyril Cohen
    1.0.4
    CeCILL-B
    Used by 3 other packages
    23 Feb 2026
  14. rocq-mathcomp-boot

    No documentation

    Small Scale Reflection
    keyword:small scale reflection keyword:mathematical components keyword:bigop keyword:big operators keyword:biomial coefficient keyword:integer division theory keyword:finite sets keyword:functions with finite domain keyword:finite graphs keyword:quotient types keyword:lists keyword:ordering and sorting lists keyword:prime numbers keyword:tuples keyword:bounded lists logpath:mathcomp.boot
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 8 other packages
    13 Nov 2025
  15. rocq-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.5.0
    CECILL-B
    Used by 1 other packages
    13 Nov 2025
  16. rocq-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.16.0
    CECILL-C
    Used by 2 other packages
    16 Mar 2026
  17. rocq-mathcomp-experimental-reals

    No documentation

    A library for alternative real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.experimental_reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 1 other packages
    16 Mar 2026
  18. rocq-mathcomp-field

    No documentation

    Mathematical Components Library on Fields
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:field logpath:mathcomp.field
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 5 other packages
    13 Nov 2025
  19. rocq-mathcomp-fingroup

    No documentation

    Mathematical Components Library on finite groups
    keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.fingroup
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 5 other packages
    13 Nov 2025
  20. rocq-mathcomp-finmap

    No documentation

    Finite sets, finite maps, finitely supported functions
    keyword:finmap keyword:finset keyword:multiset logpath:mathcomp.finmap
    Cyril Cohen Kazuhiko Sakaguchi
    2.2.2
    CECILL-B
    Used by 3 other packages
    13 Nov 2025
  21. rocq-mathcomp-hollight-real-with-N

    No documentation

    HOL-Light definition of real numbers in Rocq using N and MathComp
    logpath:MathComp_HOLLight_Real_With_N date:2025-07-11 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers keyword:HOL-Light
    https://github.com/Deducteam/mathcomp-hollight-real-with-N/blob/main/AUTHORS.md
    0.0.0
    CeCILL-2.1
    Used by 2 other packages
    02 Oct 2025
  22. rocq-mathcomp-order

    No documentation

    Mathematical Components Library on order theory
    keyword:small scale reflection keyword:mathematical components keyword:order theory keyword:partial order keyword:lattices keyword:total order logpath:mathcomp.order
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 6 other packages
    13 Nov 2025
  23. rocq-mathcomp-reals

    No documentation

    A library for real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals keyword:extended real numbers logpath:mathcomp.reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 4 other packages
    16 Mar 2026
  24. rocq-mathcomp-reals-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 2 other packages
    16 Mar 2026
  25. rocq-mathcomp-solvable

    No documentation

    Mathematical Components Library on finite groups (II)
    keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.solvable
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 5 other packages
    13 Nov 2025
  26. rocq-mathcomp-ssreflect

    No documentation

    Compatibility package for rocq-mathcomp-boot and rocq-mathcomp-order
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 5 other packages
    13 Nov 2025
  27. rocq-metarocq

    No documentation

    A meta-programming framework for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 0 other packages
    12 Mar 2026
  28. rocq-metarocq-common

    No documentation

    The common library of Template Rocq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  29. rocq-metarocq-erasure

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  30. rocq-metarocq-erasure-plugin

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  31. rocq-metarocq-pcuic

    No documentation

    A type system equivalent to Rocq's and its metatheory
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  32. rocq-metarocq-quotation

    No documentation

    Gallina quotation functions for Template Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 1 other packages
    12 Mar 2026
  33. rocq-metarocq-safechecker

    No documentation

    Implementation and verification of safe conversion and typechecking algorithms for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  34. rocq-metarocq-safechecker-plugin

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 2 other packages
    12 Mar 2026
  35. rocq-metarocq-template

    No documentation

    A quoting and unquoting library for Rocq in Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  36. rocq-metarocq-template-pcuic

    No documentation

    Translations between Template Rocq and PCUIC and proofs of correctness
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 5 other packages
    12 Mar 2026
  37. rocq-metarocq-translations

    No documentation

    Translations built on top of MetaRocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 1 other packages
    12 Mar 2026
  38. rocq-metarocq-utils

    No documentation

    The utility library of Template Rocq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  39. rocq-micromega-plugin

    No documentation

    Micromega plugin for Rocq
    category:Miscellaneous/Rocq Extensions keyword:micromega logpath:micromega-plugin
    Frederic Besson
    1.0.0
    LGPL-2.1
    Used by 0 other packages
    16 Apr 2026
  40. rocq-monae

    No documentation

    Monads and equational reasoning in Rocq
    keyword:monae keyword:effects keyword:probability keyword:nondeterminism logpath:monae date:2026-04-07
    Reynald Affeldt David Nowak Takafumi Saikawa Jacques Garrigue Ayumu Saito et al.
    0.9.2
    LGPL-2.1-or-later
    Used by 1 other packages
    21 Apr 2026
  41. rocq-navi

    No documentation

    Extension of coq2html Document Generator
    category:Tools/Document Generator keyword:document keyword:html logpath:
    Xavier Leroy Reynald Affeldt <reynald.affeldt@aist.go.jp> Yoshihiro Imai <y.imai@aist.go.jp>
    0.4.1
    GPL-2.0-or-later
    Used by 0 other packages
    18 Mar 2026
  42. rocq-num-analysis

    No documentation

    Numerical analysis in Rocq
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 0 other packages
    13 Mar 2026
  43. rocq-num-analysis-algebra

    No documentation

    Algebraic structures for numerical analysis in Rocq
    category:Mathematics/Algebra date:2026-03 logpath:NumAnalysis.Algebra keyword:algebra keyword:algebraic structure hierarchy keyword:functions to an algebraic structure keyword:algebraic substructure keyword:morphism keyword:monoid keyword:group keyword:ring keyword:module space keyword:affine space keyword:dimension theorem keyword:incomplete basis theorem keyword:dual basis keyword:predual basis keyword:rank-nullity theorem keyword:binomial coefficient
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 2 other packages
    13 Mar 2026
  44. rocq-num-analysis-fem

    No documentation

    The finite element method
    category:Mathematics/Real Calculus and Topology date:2026-03 logpath:NumAnalysis.FEM keyword:multi-index keyword:multi-variate polynomial keyword:Lagrange polynomial keyword:finite element keyword:simplicial Lagrange finite element
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    13 Mar 2026
  45. rocq-num-analysis-lax-milgram

    No documentation

    Lax-Milgram theorem
    category:Mathematics/Real Calculus and Topology date:2026-03 logpath:NumAnalysis.LM keyword:fixed point theorem (in a Banach space) keyword:orthogonal projection keyword:orthogonal complement keyword:Riesz-Fréchet representation theorem keyword:Lax-Milgram theorem keyword:Céa's lemma
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    13 Mar 2026
  46. rocq-num-analysis-lebesgue

    No documentation

    Lebesgue integral
    category:Mathematics/Real Calculus and Topology date:2026-03 logpath:NumAnalysis.Lebesgue keyword:sigma-algebra keyword:monotone class theorem keyword:Dynkin pi-lambda theorem keyword:measure theory keyword:Lebesgue measure keyword:simple function keyword:adapted sequence keyword:Beppo Levi (monotone convergence) theorem keyword:Fatou lemma keyword:Lebesgue (dominated convergence) theorem keyword:Lebesgue induction principle keyword:Tonelli theorem keyword:Bochner integral
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    13 Mar 2026
  47. rocq-num-analysis-subset

    No documentation

    Subsets for numerical analysis in Rocq
    category:Mathematics/Logic/Set theory date:2026-03 logpath:NumAnalysis.Requisite logpath:NumAnalysis.Logic logpath:NumAnalysis.Numbers logpath:NumAnalysis.Subsets keyword:subset keyword:function keyword:homogeneous binary relation keyword:operation on finite families
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 2 other packages
    13 Mar 2026
  48. rocq-ollibs

    No documentation

    OL libraries
    keyword:standard library keyword:list keyword:permutation keyword:decidable equality keyword:finite multiset category:Mathematics/Combinatorics and Graph Theory date:2025-11-11 logpath:OLlibs
    Olivier Laurent Christophe Lucas
    2.1.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Nov 2025
  49. rocq-parseque

    No documentation

    Total parser combinators in Rocq/Coq
    category:Computer Science/Data Types and Data Structures date:2025-06-24 logpath:parseque
    G. Allais
    0.3.0
    MIT
    Used by 0 other packages
    27 Jun 2025
  50. rocq-pi-agm

    No documentation

    Computing thousands or millions of digits of PI with arithmetic-geometric means
    keyword:real analysis keyword:pi category:Mathematics/Real Calculus and Topology logpath:agm date:2020-06-23
    Yves Bertot <yves.bertot@inria.fr>
    1.2.9
    CECILL-B
    Used by 0 other packages
    14 Aug 2025
... 10 11 12