Kruskal and Higman type tree theorems for the Kruskal-AlmostFull library

An adaptation of Wim Veldman's proof of the tree theorem to Coq

Detailed proof of Higman's lemma for unary trees and lists

The Fan theorem for inductive bars and a constructive variant of König's lemma

Library of basic results about Almost Full relations in Coq

Hilbert Basis Theorem in Coq/Rocq

Tools for dealing with finiteness and choice

Coq library for rose trees

Coq artifact for "Constructive substitutes for König's lemma"

Hercules kills the Hydra in Coq

The well-foundedness of the multiset ordering

Failing SQLite3 DB

Euclide et l'irrationalité de ⁿ√k pour k différent de rⁿ

Description of the Coq-Kruskal project with a map and pointers

Construction of Friedman's tree(n) and TREE(n) in Coq

A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull

Quasi morphisms for Almost Full relations

Wim Veldman's stumps for almost full relations in inductive type theory

The Braga Method for Extracting Certified OCaml from Coq code

Extraction of µ-recursive algorithms in Coq

A clean and short proof of strong normalization for Curry-style System F

Introduction to the Coq proof assistant

The square root of 2 is not rational

A short Coq proof of the PHP

A small course on the inductive accessibility predicate in Coq

Direct proof that strict orders on listable types are well-founded

A constructive account of Kripke-Curry's decidability proof for Implicational Relevance logic (see README.md below)