Lean4
/-- A version of `withRWRulesSeq` (in core) that doesn't attempt to find equation lemmas, and simply
passes the rw rules on to `x`. -/
def withSimpRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) :
TacticM Unit := do
let lbrak := rwRulesSeqStx[0]
let rules := rwRulesSeqStx[1].getArgs
withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
let numRules := (rules.size + 1) / 2
for i in [:numRules]do
let rule := rules[i * 2]!
let sep := rules.getD (i * 2 + 1) Syntax.missing
withTacticInfoContext (mkNullNode #[rule, sep]) do
-- show errors on rule
withRef rule do
let symm := !rule[0].isNone
let term :=
rule[1]
-- let processId (id : Syntax) : TacticM Unit := do
x symm term
