13 search results for "tag:"keyword:finite""
Showing 1 - 13
-
coq-atbr
No documentation
Coq library and tactic for deciding Kleene algebras8.20.0LGPL-3.0-or-laterUsed by 0 other packages06 Sep 2024 -
coq-color
No documentation
A library on rewriting theory and terminationdate: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 theorem1.8.5CeCILL-2.1Used by 0 other packages16 Apr 2024 -
coq-extructures
No documentation
Finite sets, maps, and other data structures with extensional reasoning0.5.0MITUsed by 1 other packages10 Dec 2024 -
coq-mathcomp-algebra
No documentation
Mathematical Components Library on Algebrakeyword: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.algebra2.3.0CECILL-BUsed by 29 other packages29 Nov 2024 -
coq-mathcomp-fingroup
No documentation
Mathematical Components Library on finite groups2.3.0CECILL-BUsed by 11 other packages29 Nov 2024 -
coq-mathcomp-odd-order
No documentation
The formal proof of the Feit-Thompson theorem2.0.0CeCILL-BUsed by 0 other packages18 Oct 2023 -
coq-mathcomp-solvable
No documentation
Mathematical Components Library on finite groups (II)2.3.0CECILL-BUsed by 7 other packages29 Nov 2024 -
coq-mathcomp-ssreflect
No documentation
Small Scale Reflectionkeyword: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.ssreflect2.3.0CECILL-BUsed by 40 other packages29 Nov 2024 -
coq-mmaps
No documentation
Several implementations of finite maps over arbitrary ordered types using Coq functors1.1LGPL-2.1-onlyUsed by 0 other packages08 Jan 2024 -
coq-msets-extra
No documentation
Extensions of MSets for Efficient Execution1.2.0LGPL-2.1-onlyUsed by 0 other packages19 Sep 2019 -
coq-ollibs
No documentation
OL libraries2.0.7LGPL-3.0-or-laterUsed by 0 other packages17 Sep 2024 -
coq-reglang
No documentation
Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp1.2.1CECILL-BUsed by 1 other packages19 Jan 2024 -
coq-zorns-lemma
No documentation
This library develops some basic set theory in Coq10.2.0LGPL-2.1-or-laterUsed by 1 other packages21 Aug 2023