matafou Goto Github PK

chord_finder

A small tool to find chords from lists of music notes, written in A B C or in "Figured bass" notations

circul-mode

compcert

The CompCert C verified compiler

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-label

Labels for Coq

coq-www

Source files of the coq.inria.fr website (static part)

corn

Coq Repository at Nijmegen

glapi

Gitlab API from bash (based on jq)

ill_narratives

A development of a subset of intuitionistic linear logic, suitable for representing narratives.

landmark

Emacs package provinding fast navigation between buffers/positions.

libhyps

A Coq library providing tactics to deal with hypothesis

math-comp

Mathematical Components

nfp121.tpinjection

TP injection de dépendances pour NFP121 et GLG204

normalizedtypes

Implementing normalized types using the coq v8.10's Sprop feature.

opam-coq-archive

Archive for all Coq related OPAM packages organized in various repositories

pg

New home of Proof-General (http://proofgeneral.inf.ed.ac.uk/)

r_article

sparkcompcert

sparkformal

The project SPARK Formal aims at developing a complete semantics of the SPARK language in Coq.

tacmaphyp

A library for automatic namnig if hypothesis in Coq. Entirely written in Ltac.

unimath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.