def Std.Tactic.check_tactic_goal : Lean.ParserDescr

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.

def Std.Tactic.«command#check_tactic_~>_By_» : Lean.ParserDescr

#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.

def Std.Tactic.«command#check_simp_~>_» : Lean.ParserDescr

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

Equations

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