270 search results for "tag:"logpath:""

Showing 251 - 270
  1. 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.4.0
    CECILL-B
    Used by 1 other packages
    15 Apr 2025
  2. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  3. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  4. 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.1
    CECILL-B
    Used by 2 other packages
    29 Apr 2025
  5. 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
  6. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  7. rocq-mathcomp-ssreflect

    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:order theory keyword:partial order keyword:lattices keyword:lists keyword:ordering and sorting lists keyword:prime numbers keyword:tuples keyword:bounded lists logpath:mathcomp.ssreflect
    The Mathematical Components team
    2.4.0
    CECILL-B
    Used by 4 other packages
    15 Apr 2025
  8. 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.3.1
    GPL-2.0-or-later
    Used by 0 other packages
    17 Sep 2025
  9. rocq-num-analysis-algebra

    No documentation

    Algebraic structures for numerical analysis in Rocq
    category:Math/Algebra date:2025-06 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.0.0
    LGPL-3.0-or-later
    Used by 2 other packages
    23 Jun 2025
  10. rocq-num-analysis-fem

    No documentation

    The finite element method
    category:Math/Real Calculus and Topology date:2025-06 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.0.0
    LGPL-3.0-or-later
    Used by 1 other packages
    23 Jun 2025
  11. rocq-num-analysis-lax-milgram

    No documentation

    Lax-Milgram theorem
    category:Math/Real Calculus and Topology date:2025-06 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.0.0
    LGPL-3.0-or-later
    Used by 1 other packages
    23 Jun 2025
  12. rocq-num-analysis-lebesgue

    No documentation

    Lebesgue integral
    category:Math/Real Calculus and Topology date:2025-06 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.0.0
    LGPL-3.0-or-later
    Used by 1 other packages
    23 Jun 2025
  13. rocq-num-analysis-subset

    No documentation

    Subsets for numerical analysis in Rocq
    category:Math/Logic/Set theory date:2025-06 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.0.0
    LGPL-3.0-or-later
    Used by 2 other packages
    23 Jun 2025
  14. rocq-ollibs

    No documentation

    OL libraries
    keyword:standard library keyword:list keyword:permutation keyword:decidable equality keyword:finite multisets category:Mathematics/Combinatorics and Graph Theory date:2025-04-22 logpath:OLlibs
    Olivier Laurent Christophe Lucas
    2.1.0
    LGPL-3.0-or-later
    Used by 0 other packages
    23 Apr 2025
  15. 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
  16. 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
  17. rocq-relation-algebra

    No documentation

    Relation Algebra and KAT in Rocq
    keyword:relation algebra keyword:Kleene algebra with tests keyword:KAT keyword:allegories keyword:residuated structures keyword:automata keyword:regular expressions keyword:matrices category:Mathematics/Algebra logpath:RelationAlgebra
    Damien Pous <Damien.Pous@ens-lyon.fr> Christian Doczkal <christian.doczkal@ens-lyon.fr>
    1.8.0
    LGPL-3.0-or-later
    Used by 1 other packages
    19 Sep 2025
  18. rocq-rouche-capelli

    No documentation

    A proof for the Rouché–Capelli theorem by rocq-math-comp
    category:Mathematics/Algebra keyword:linear algebra keyword:matrix keyword:rank logpath:RoucheCapelli
    Cheng-Hui Weng Reynald Affeldt Jacques Garrigue Takafumi Saikawa
    0.1.0
    MIT
    Used by 0 other packages
    24 Oct 2025
  19. rocq-vellvm

    No documentation

    Rocq library implementing (executable) semantics for LLVM IR
    date:2025-07-10 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm
    Steve Zdancewic <stevez@cis.upenn.edu> Yannick Zakowski <yannick.zakowski@inria.fr> Calvin Beck <hobbes@seas.upenn.edu> Irene Yoon <euisuny@cis.upenn.edu> Gary (Hanxi) Chen <hanxic@seas.upenn.edu>
    v2.2.20250710
    GPL-3.0-or-later
    Used by 0 other packages
    18 Jul 2025
  20. rocq-yalla

    No documentation

    Yalla library
    keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2025-03-26 logpath:Yalla
    Olivier Laurent
    2.0.7
    LGPL-3.0-or-later
    Used by 0 other packages
    27 Mar 2025
... 4 5 6