Matita HomeMatita Home+ The system shares a common look&feel with the Coq proof assistant + and its graphical user interface. The two systems have variants + of the same logic, + close proof languages and similar sets of tactics. + From the user point of view the main lacking features + with respect to Coq are: +
proof extraction;
an extensible language of tactics;
automatic implicit arguments;
several ad-hoc decision procedures;
several rarely used variants for most of the tactics;
sections and local variables.
+ Still from the user point of view, the main differences with respect + to Coq are: +
the language of tacticals that allows execution of partial tactical application;
the unification of the concept of metavariable and existential variable;
terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;
ambiguous terms are disambiguated by direct interaction with the user;
theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.