Ltac¶

Goal & context management¶

Automatic variable naming¶

Do not rely on Coq’s automatically generated names.
Consider enabling Mangle Names.

Braces and bullets¶

TODO

No epic proofs¶

TODO

Destruct patterns¶

TODO

Defining custom tactics¶

TODO

`Tactic Notation`¶

TODO

Guidance on specific tactics¶

`intros`, `revert`, `rename`, `clear`¶

TODO

`admit`, `give_up`¶

TODO

`easy`, `now`, `assumption`, `trivial`¶

TODO

`try`¶

TODO

`lia`, `nia`¶

TODO

`left`, `right`, `exists`, `constructor`¶

TODO

`reflexivity`, `symmetry`, `transitivity`, `congruence`¶

TODO

`absurd`, `contradiction`, `exfalso`¶

TODO

`exact`, `apply`, `refine`¶

TODO

`simpl`, `red`, `cbv`¶

TODO

`rewrite`, `subst`¶

TODO

`assert ... as`, `enough`¶

TODO

`pose proof ... as`¶

TODO

`remember ... as`¶

TODO

`change ... with`¶

TODO

`generalize`¶

TODO

`specialize`¶

TODO

`auto`¶

TODO

`eintros`, `evar`, `eauto`, `erefine`, `eassumption`, `eenough`, `instantiate`¶

TODO