Lean4
/-- `move_oper_simpCtx` is the `Simp.Context` for the reordering internal to `move_oper`.
To support a new binary operation, extend the list in this definition, so that it contains
enough lemmas to allow `simp` to close a generic permutation goal for the new binary operation.
-/
def moveOperSimpCtx : MetaM Simp.Context := do
let simpNames :=
Elab.Tactic.simpOnlyBuiltins ++
[``add_comm, ``add_assoc, ``add_left_comm, -- for `HAdd.hAdd`
``mul_comm, ``mul_assoc, ``mul_left_comm, -- for `HMul.hMul`
``and_comm, ``and_assoc, ``and_left_comm, -- for `and`
``or_comm, ``or_assoc, ``or_left_comm, -- for `or`
``max_comm, ``max_assoc, ``max_left_comm, -- for `max`
``min_comm, ``min_assoc, ``min_left_comm]
let simpThms ← simpNames.foldlM (·.addConst ·) ({ } : SimpTheorems)
Simp.mkContext { } (simpTheorems := #[simpThms])
