@[reduce_mod_char] attribute

This file registers @[reduce_mod_char] as a simp attribute.

opaque reduceModCharExt : Lean.Meta.SimpExtension

@[reduce_mod_char] is an attribute that tags lemmas for preprocessing and cleanup in the reduce_mod_char tactic