• Stars
    star
    1
  • Language Coq
  • Created over 7 years ago
  • Updated over 1 year ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Formalizing Cylindrical Algebraic Decomposition related theories in mathcomp

More Repositories

1

math-comp

Mathematical Components
Coq
562
star
2

analysis

Mathematical Components compliant Analysis Library
Coq
194
star
3

mcb

Mathematical Components (the Book)
TeX
139
star
4

hierarchy-builder

High level commands to declare a hierarchy based on packed classes
Prolog
95
star
5

finmap

Finite sets, finite maps, multisets and generic sets
Coq
46
star
6

Coq-Combi

Algebraic Combinatorics in Coq
Coq
34
star
7

algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
Coq
29
star
8

Abel

A proof of Abel-Ruffini theorem.
Coq
28
star
9

odd-order

The formal proof of the Odd Order Theorem
Coq
24
star
10

mczify

Micromega tactics for Mathematical Components
Coq
22
star
11

tutorial_material

proof script associated to tutorial material
Coq
17
star
12

multinomials

Multinomials for the Mathematical Components library.
Coq
14
star
13

real-closed

Theorems for Real Closed Fields
Coq
13
star
14

POPLmark

Solutions for the POPLmark challenge
Coq
7
star
15

math-comp.github.io

https://math-comp.github.io/
HTML
7
star
16

docker-mathcomp

Docker images of coq-mathcomp [maintainer=@erikmd]
Dockerfile
6
star
17

bigenough

Asymptotic reasoning with bigenough
Coq
4
star
18

wiki

general wiki of the math-comp organization
3
star
19

mathcomp-history-before-github

The "coqfinitgroup" repository before the switch to github
Coq
3
star
20

dioid

A formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).
Coq
3
star
21

ssr-manual

SSReflect user manual
PostScript
3
star
22

math-comp-nix

Nix support for mathcomp packages
Nix
1
star
23

newtonsums

Newton series transformation
Coq
1
star