LambdaPi Search Engine

This web page offers facilities to search objects in the HOL-Light Multivariate library through its translation to Lambdapi using the hol2dk.

This library contains 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 resulting definitions and theorems have also been translated to Coq using Lambdapi and gathered in the Opam package coq-hol-light.

The search button answers the query. The syntax of queries and terms is available in the Lambdapi user manual through the following links: queries and terms.

Examples of terms:

• λ (x:A) y z,t: anonymous function mapping x (of type A), y and z to t.
• Π (x:A) y z,T: dependent product.
• A → T: non-dependent product (syntactic sugar for Π x:A,T when x does not occur in T).

Examples of queries:

• hyp = (num → num) , hyp >= Real searches for all objects having as hypothesis a function of type num → num and such that Real occurs in some (possibly other) hypothesis.
• concl > real_of_num | HOLLight.theorems searches for all objects having an hypothesis containing real_of_num and located in a module whose path is a suffix of HOLLight.theorems
• name = num ; name = NUM searches for all objects whose name is either num or NUM

For commodity, it is possible to use "forall" and "->" instead of "Π" and "→" respectively (Results are displayed with the Unicode symbols "Π" and "→").