Normalisation Rules #
Safe and Almost Safe Rules #
Unsafe Rules #
Regular Rules #
- safe (r : SafeRule) : RegularRule
- unsafe (r : UnsafeRule) : RegularRule
Instances For
@[inline]
Equations
Instances For
Normalisation Simp Rules #
A global rule for the norm simplifier. Each SimpEntry
represents a member
of the simp set, e.g. a declaration whose type is an equality or a smart
unfolding theorem for a declaration.
- name : RuleName
- entries : Array Lean.Meta.SimpEntry
Instances For
A local rule for the norm simplifier.