def Batteries.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 Batteries.Tactic.check_tactic_fails : 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 Batteries.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 Batteries.Tactic.«command#check_simp_~>_» : Lean.ParserDescr

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

Equations

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

def Batteries.Tactic.«command#check_simp_!~>» : Lean.ParserDescr

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

Equations

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