Documentation

Mathlib.Tactic.FieldSimp.Attr

Attribute grouping the field_simp simprocs #

opaque fieldSimpExt :
Lean.Meta.Simp.SimprocExtension

Initialize the attribute field grouping the simprocs associated to the field_simp tactic.