This web page offers facilities to search objects in the HOL-Light library translated and available in Dedukti, Lambdapi and Coq/Rocq.
The translation has been performed using the hol2dk tool and the resulting theorems are gathered in the Opam package coq-hol-light available in the Coq Opam repository released. It currently contains a translation of the Multivariate library with more than 20,000 theorems on arithmetic, wellfounded relations, lists, real numbers, integers, basic set theory, permutations, group theory, matroids, metric spaces, homology, vectors, determinants, topology, convex sets and functions, paths, polytopes, Brouwer degree, derivatives, Clifford algebra, integration, measure theory, complex numbers and analysis, transcendental numbers, real analysis, complex line integrals, etc.
The search button answers the query. Read the query
language specification to learn about the query language.