- name : Lean.Name
- scope : ScopeName
- builders : Array BuilderName
#[]
means 'match any builder' #[]
means 'match any phase'
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Returns the identifier of the local norm simp rule matched by f
, if any.