Documentation

Lean.Meta.Tactic.Simp.Rewrite

Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.

Instances For