487 search results for ""

Showing 251 - 300
  1. coq-lens

    No documentation

    Generation of lenses for record datatypes
    logpath:Lens date: 2020-11-18
    Gregory Malecha <gregory@bedrocksystems.com>
    1.0.1+8.12
    LGPL2.1+BedRock
    Used by 0 other packages
    18 Nov 2020
  2. coq-lesniewski-mereology

    No documentation

    Knowledge-based Dependently Typed Language (KDTL)
    keyword: mereology keyword: protothetic keyword: ontology keyword: nominalist theory keyword: extensionality category: Mathematics/Logic/Foundations
    Richard Dapoigny <richard.dapoigny@univ-savoie.fr> [https://www.researchgate.net/profile/Richard_Dapoigny] Patrick Barlatier <patrick.barlatier@univ-savoie.fr> [https://www.researchgate.net/profile/Patrick_Barlatier]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  3. coq-libhyps

    No documentation

    Hypotheses manipulation library
    keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming category:Miscellaneous/Coq Extensions logpath:LibHyps date:2024-12-19
    Pierre Courtieu
    3.0.1
    MIT
    Used by 1 other packages
    19 Dec 2024
  4. coq-library-complexity

    No documentation

    A Coq Library of Complexity Theory
    Fabian Kunze Lennard Gäher Maximilian Wuttke Yannick Forster Stefan Haan
    1.0+8.16
    CECILL-2.1
    Used by 0 other packages
    09 Nov 2022
  5. coq-library-fol

    No documentation

    A Coq Library for First-Order Logic
    Dominik Kirst Johannes Hostert Andrej Dudenhefner Yannick Forster Marc Hermes et al.
    1.0+8.20
    MIT
    Used by 0 other packages
    06 Feb 2025
  6. coq-library-undecidability

    No documentation

    A Coq Library of Undecidability Proofs
    Yannick Forster Dominique Larchey-Wendling Andrej Dudenhefner Edith Heiter Marc Hermes et al.
    1.1.2+8.20
    MPL-2.0
    Used by 1 other packages
    30 Sep 2024
  7. 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.4
    LGPL-2.1-or-later
    Used by 1 other packages
    07 Feb 2025
  8. coq-lin-alg

    No documentation

    Linear Algebra
    keyword: linear algebra category: Mathematics/Algebra date: 19 spetember 2003
    Jasper Stein <jasper@cs.kun.nl>
    8.9.0
    LGPL 2.1
    Used by 1 other packages
    08 Dec 2019
  9. coq-linearscan

    No documentation

    A linear scan register allocator in Coq
    keyword: register allocator category:Computer Science/Semantics and Compilation/Compilation date: 2022-07-23 logpath: Linearscan
    John Wiegley
    1.1.0
    BSD-3-Clause
    Used by 0 other packages
    23 Jul 2022
  10. coq-list-plus

    No documentation

    More functions on lists
    Guillaume Claret
    1.1.0
    MIT
    Used by 1 other packages
    25 Nov 2015
  11. coq-list-string

    No documentation

    Strings implemented as lists
    Guillaume Claret
    2.1.2
    MIT
    Used by 8 other packages
    07 May 2019
  12. coq-ltac-iter

    No documentation

    Access hint databases from tactics
    Gregory Malecha
    1.1.2
    MIT
    Used by 0 other packages
    03 Jun 2020
  13. coq-ltac2

    No documentation

    A tactic language for Coq
    Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
    0.3
    LGPL 2.1
    Used by 0 other packages
    07 Jun 2019
  14. coq-ltl

    No documentation

    Linear Temporal Logic
    keyword: temporal logic keyword: infinite transition systems keyword: co-induction category: Mathematics/Logic/Modal logic date: 2002-07
    Solange Coupet-Grimal
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  15. coq-maple-mode

    No documentation

    A Maple Mode for Coq
    keyword: Maple keyword: simplification keyword: field tactic category: Miscellaneous/Coq Extensions date: 2002-03
    David Delahaye Micaela Mayero
    8.9.0
    Unknown
    Used by 0 other packages
    08 Dec 2019
  16. coq-markov

    No documentation

    Markov's inequality
    keyword: probability keyword: Markov keyword: Lebesgue integration keyword: sigma algebras keyword: measurability keyword: Borel category: Mathematics/Real Calculus and Topology date: 2008-01-5
    Robert Kam <rkam2001@hotmail.com> [none]
    8.10.0
    GNU Lesser Public License
    Used by 0 other packages
    07 Dec 2019
  17. coq-math-classes

    No documentation

    A library of abstract interfaces for mathematical structures in Coq
    logpath:MathClasses date:2024-04-23
    Eelis van der Weegen Bas Spitters Robbert Krebbers
    8.19.0
    MIT
    Used by 1 other packages
    23 Apr 2024
  18. coq-mathcomp-abel

    No documentation

    Abel - Ruffini's theorem
    keyword:algebra keyword:Galois keyword:Abel Ruffini keyword:unsolvability of quintincs logpath:Abel date:2022-07-13
    Sophie Bernard Cyril Cohen Assia Mahboubi Pierre-Yves Strub
    1.2.1
    CECILL-B
    Used by 0 other packages
    24 Oct 2022
  19. 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 32 other packages
    29 Nov 2024
  20. coq-mathcomp-algebra-tactics

    No documentation

    Ring, field, lra, nra, and psatz tactics for Mathematical Components
    logpath:mathcomp.algebra_tactics
    Kazuhiko Sakaguchi Pierre Roux
    1.2.4
    CECILL-B
    Used by 2 other packages
    25 Jan 2025
  21. 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.9.0
    CECILL-C
    Used by 7 other packages
    20 Feb 2025
  22. coq-mathcomp-analysis-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.9.0
    CECILL-C
    Used by 0 other packages
    20 Feb 2025
  23. 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
  24. coq-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.2
    CeCILL-B
    Used by 8 other packages
    25 Jan 2025
  25. 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
  26. 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
  27. 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.9.0
    CECILL-C
    Used by 2 other packages
    20 Feb 2025
  28. 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
  29. coq-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.9.0
    CECILL-C
    Used by 1 other packages
    20 Feb 2025
  30. coq-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.3.0
    CECILL-B
    Used by 12 other packages
    29 Nov 2024
  31. coq-mathcomp-field-extra

    No documentation

    Extra Mathematical Components Library on Fields
    keyword:algebra keyword:field keyword:small scale reflection keyword:mathematical components keyword:odd order theorem
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    1.6.1
    CeCILL-B
    Used by 1 other packages
    26 Jun 2019
  32. coq-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.3.0
    CECILL-B
    Used by 11 other packages
    29 Nov 2024
  33. coq-mathcomp-finmap

    No documentation

    Finite sets, finite maps, finitely supported functions
    keyword:finmap keyword:finset keyword:multiset date:2024-01-17 logpath:mathcomp.finmap
    Cyril Cohen Kazuhiko Sakaguchi
    2.1.0
    CECILL-B
    Used by 6 other packages
    17 Jan 2024
  34. coq-mathcomp-multinomials

    No documentation

    A Multivariate polynomial Library for the Mathematical Components Library
    keyword:multinomials keyword:monoid algebra category:Mathematics/Algebra/Multinomials category:Mathematics/Algebra/Monoid algebra logpath:mathcomp.multinomials
    Pierre-Yves Strub
    2.3.0
    CECILL-B
    Used by 3 other packages
    14 Dec 2024
  35. coq-mathcomp-odd-order

    No documentation

    The formal proof of the Feit-Thompson theorem
    keyword:finite groups keyword:Feit Thompson theorem keyword:small scale reflection keyword:mathematical components keyword:odd order theorem
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    2.1.0
    CeCILL-B
    Used by 0 other packages
    04 Jan 2025
  36. coq-mathcomp-real-closed

    No documentation

    Mathematical Components Library on real closed fields
    keyword:real closed field logpath:mathcomp.real_closed date:2024-12-09
    Cyril Cohen Assia Mahboubi
    2.0.2
    CECILL-B
    Used by 5 other packages
    14 Dec 2024
  37. coq-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.9.0
    CECILL-C
    Used by 3 other packages
    20 Feb 2025
  38. coq-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.9.0
    CECILL-C
    Used by 4 other packages
    20 Feb 2025
  39. coq-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.3.0
    CECILL-B
    Used by 7 other packages
    29 Nov 2024
  40. coq-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.3.0
    CECILL-B
    Used by 45 other packages
    29 Nov 2024
  41. coq-mathcomp-sum-of-two-square

    No documentation

    A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :
    logpath:mathcomp.contrib.sum_of_two_square
    Laurent Thery
    1.0.1
    MIT
    Used by 0 other packages
    09 May 2018
  42. coq-mathcomp-tarjan

    No documentation

    Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
    category:Computer Science/Graph Theory keyword:strongly connected components keyword:topological sorting keyword:Kosaraju keyword:Tarjan keyword:acyclicity keyword:graph theory logpath:mathcomp.tarjan date:2023-08-06
    Cyril Cohen Jean-Jacques Lévy Karl Palmskog Laurent Théry
    1.0.2
    CECILL-B
    Used by 0 other packages
    06 Aug 2023
  43. coq-mathcomp-word

    No documentation

    Yet Another Coq Library on Machine Words
    category:Computer Science/Data Types and Data Structures keyword:machine words logpath:mathcomp.word date:2024-03-21
    Pierre-Yves Strub
    3.2
    MIT
    Used by 0 other packages
    11 Jun 2024
  44. coq-mathcomp-zify

    No documentation

    Micromega tactics for Mathematical Components
    logpath:mathcomp.zify
    Kazuhiko Sakaguchi
    1.5.0+2.0+8.16
    CECILL-B
    Used by 5 other packages
    12 Jul 2023
  45. coq-maths

    No documentation

    Basic mathematics
    keyword: mathematics category: Mathematics/Arithmetic and Number Theory/Number theory
    Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  46. coq-matrices

    No documentation

    Ring properties for square matrices
    keyword: matrices keyword: vectors keyword: linear algebra keyword: Coq modules category: Mathematics/Algebra date: 2003-03
    Nicolas Magaud
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  47. coq-matrix

    No documentation

    Formal matrix theory with multiple implementations in Coq
    keyword:matrices category:Mathematics/Algebra date:2024-01-16 logpath:CoqMatrix
    ZhengPu Shi
    1.0.6
    MIT
    Used by 0 other packages
    16 Jan 2024
  48. coq-menhirlib

    No documentation

    A support library for verified Coq parsers produced by Menhir
    date:2024-07-15 logpath:MenhirLib
    Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>
    20240715
    LGPL-3.0-or-later
    Used by 5 other packages
    15 Jul 2024
  49. coq-metacoq

    No documentation

    A meta-programming framework for Coq
    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.3.4+9.0
    MIT
    Used by 0 other packages
    03 Apr 2025
  50. coq-metacoq-common

    No documentation

    The common library of Template Coq 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.3.4+9.0
    MIT
    Used by 4 other packages
    03 Apr 2025
... 5 6 7 ... 10