Proof assistant for higher-order logic
Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.
Identify input labels that do not match package names
|label 'lablgtk3' does not match package name 'lablgtk'|
Validate file names and availability of patches
|file names of patches should start with the package name|