thery Goto Github PK

alectryon

A collection of tools for writing technical documents that mix Coq code and prose.

analysis

Mathematical Components compliant Analysis Library

atom-language-coq

Coq language support for the Atom editor

bbv

Bedrock Bit Vector Library

bignums

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

ceps

Coq Enhancement Proposals

cfrac

Continuous fraction in coq

cheby

continuity

Quantitative continuity and computable analysis in Coq

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

coq-robot

coq_jupyter

Material for Coq under jupyter

coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

coqprime

Prime numbers for Coq

coquelicot

dwarith

DoubleWordArithmetic

edwardsellipticcurve

Group Law for Elliptic Curves according to Tom Hales

expfloat

exploit-plugin

An OCaml version of the LTac "exploit" tactic, used as a tutorial for writing Coq plugins

finmap

Finite sets, finite maps, multisets and generic sets

flocqlecture

fourier

fourinarow

The proof that Four is a row is a perfect game in Coq

fungrim

Fungrim: the Mathematical Functions Grimoire

gchq

Sat for GCHQ

geocoq

A formalization of geometry in Coq based on Tarski's axiom system

geometricalgebra

Work based on http://www-sop.inria.fr/marelle/GeometricAlgebra/

grobner

A fornalisation of Grobner basis in ssreflect

hanoi

Hanoi tower in Coq

hierarchy-builder

High level commands to declare a hierarchy based on packed classes