MPCTT

Commands used

Definitions

Definition, Fixpoint
Fact, Lemma, Theorem, Corollary, Example, Goal
Proof, Qed, Defined, Admitted, Abort, Show Proof

Implicit arguments, implicit types, simplification

Arguments, Implicit Types, Opaque

Sections

Section, Variable, End

Modules

Module, End, Import, Parameter
From Coq Require Import Lia

Notation

Notation

Services

Check, Compute, Eval, Scheme
Print, Print All, About, Locate, Search, Search concl:
Print Assumptions

System settings

Set Printing All, Implicit, Universes
Unset Printing …
Unset Elimination Schemes

Demo

Fail, Restart