Proof Assistant based on the Calculus of Inductive Constructions
Proof assistant which allows to handle calculus assertions, check mechanically
proofs of these assertions, helps to find formal proofs and extracts a certified
program from the constructive proof of its formal specification.
This package contains shared files and the command line interface.
For a graphical interface install coq-ide.
There is no official package available for openSUSE Leap 15.5