def tacticEnsure_only_goal : Lean.ParserDescr

ensure_only_goal succeeds, doing nothing, when there is exactly one goal. If there are multiple goals, ensure_only_goal fails

Equations

• tacticEnsure_only_goal = Lean.ParserDescr.node `tacticEnsure_only_goal 1024 (Lean.ParserDescr.nonReservedSymbol "ensure_only_goal" false)

def tacticSimp_alive_case_bash : Lean.ParserDescr

simp_alive_case_bash transforms a goal of the form ∀ (x₁ : Option (BitVec _)) ... (xₙ : Option (BitVec _)), ... into a goal about just BitVecs, by doing a case distinction on each Option.

Then, we simplify each goal, following the assumption that the none cases should generally be trivial, hopefully leaving us with just a single goal: the one where each option is some.

Equations

• tacticSimp_alive_case_bash = Lean.ParserDescr.node `tacticSimp_alive_case_bash 1024 (Lean.ParserDescr.nonReservedSymbol "simp_alive_case_bash" false)

def tacticSimp_alive_undef : Lean.ParserDescr

Unfold into the `undef' statements and eliminates as much as possible.

Equations

• tacticSimp_alive_undef = Lean.ParserDescr.node `tacticSimp_alive_undef 1024 (Lean.ParserDescr.nonReservedSymbol "simp_alive_undef" false)

def tacticSimp_alive_ops : Lean.ParserDescr

Equations

• tacticSimp_alive_ops = Lean.ParserDescr.node `tacticSimp_alive_ops 1024 (Lean.ParserDescr.nonReservedSymbol "simp_alive_ops" false)

def tacticOf_bool_tactic : Lean.ParserDescr

Equations

• tacticOf_bool_tactic = Lean.ParserDescr.node `tacticOf_bool_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "of_bool_tactic" false)

def tacticBv_eliminate_bool : Lean.ParserDescr

Equations

• tacticBv_eliminate_bool = Lean.ParserDescr.node `tacticBv_eliminate_bool 1024 (Lean.ParserDescr.nonReservedSymbol "bv_eliminate_bool" false)

def tacticBv_distrib : Lean.ParserDescr

Equations

• tacticBv_distrib = Lean.ParserDescr.node `tacticBv_distrib 1024 (Lean.ParserDescr.nonReservedSymbol "bv_distrib" false)

def tacticBv_auto : Lean.ParserDescr

Equations

• tacticBv_auto = Lean.ParserDescr.node `tacticBv_auto 1024 (Lean.ParserDescr.nonReservedSymbol "bv_auto" false)

def tacticAlive_auto : Lean.ParserDescr

Equations

• tacticAlive_auto = Lean.ParserDescr.node `tacticAlive_auto 1024 (Lean.ParserDescr.nonReservedSymbol "alive_auto" false)

def tacticBv_compare' : Lean.ParserDescr

Equations

• tacticBv_compare' = Lean.ParserDescr.node `tacticBv_compare' 1024 (Lean.ParserDescr.nonReservedSymbol "bv_compare'" false)