exact

exact allows users to solve goals by providing a proof object directly. This tactic will fail if the provided proof object does not prove the goal.

Syntax

(* Simple usage *)
exact I.

Examples

Before

=========================
1/1
True

exact I.

After

No more goals.

Before

n: nat
=========================
1/1
n + 5 = n + 5

exact (eq_refl (n + 5)).

After

No more goals.

Resources

Reference Documentation

---