Documentation

Std.Util.CheckTactic

check_tactic_goal t verifies that the goal has is equal to CheckGoalType t with reducible transparency. It closes the goal if so and otherwise reports an error.

It is used by #check_tactic.

Equations
  • One or more equations did not get rendered due to their size.

check_tactic_goal t verifies that the goal has is equal to CheckGoalType t with reducible transparency. It closes the goal if so and otherwise reports an error.

It is used by #check_tactic.

Equations
  • One or more equations did not get rendered due to their size.

#check_tactic t ~> r by commands runs the tactic sequence commands on a goal with t in the type and sees if the resulting expression has reduced it to r.

Equations
  • One or more equations did not get rendered due to their size.

#check_simp t ~> r checks simp reduces t to r.

Equations
  • One or more equations did not get rendered due to their size.

#check_simp t !~> checks simp fails to reduce t.

Equations
  • One or more equations did not get rendered due to their size.