try

The try tactical executes a provided tactic, catching any errors and always succeeding.

Syntax

(* Simple usage *)
try reflexivity.

Examples

Before

n: nat
=========================
1/1
n + 0 = n

try reflexivity.

After

n: nat
=========================
1/1
n + 0 = n

Alternatively,

try apply add_0_r.

No more goals.

Resources

Reference Documentation

---