simpl

simpl evaluates terms that are constructed of constant values - not variables. simpl can also partially evaluate partially-constant values.

Syntax

(* Simplify the goal as much as possible *)
simpl.

(* Simplify a hypothesis *)
simpl in H.

(* Simplify in the entire proof state *)
simpl in *.

(* Only simplify a specific term in a specific hypothesis *)
simpl (2 + 2) in H.

Examples

Before

-------------------------
1/1
2 + 2 = 1 + 3

simpl (2 + 2).

After

-------------------------
1/1
4 = 1 + 3

Resources

Reference Documentation

---