trans'

trans, with its two subgoals produced in the opposite order.

def CustomPrelude.Tactic.tacticTrans' : Lean.ParserDescr

Like trans, but generates the subgoal in the other order.

Equations

• CustomPrelude.Tactic.tacticTrans' = Lean.ParserDescr.node `CustomPrelude.Tactic.tacticTrans' 1024 (Lean.ParserDescr.nonReservedSymbol "trans'" false)