ApplySpec

This module provides the tactic applying per-instruction specifications.

def tacticApplySpecFrstGoal_ : Lean.ParserDescr

Apply an instruction specification to the first generated goal.

Equations

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

def tacticApplySpecScdGoal_ : Lean.ParserDescr

Apply an instruction specification to the second generated goal.

Equations

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