@[tendsto_cont] attribute

Environment extension and attribute registration for the tendsto_cont tactic. Separated into its own file so that meta tactic code can access the extension (which must be from a pre-compiled module).

opaque tendstoContExt : Lean.SimpleScopedEnvExtension Lean.Name Lean.NameSet

Environment extension storing @[tendsto_cont]-registered lemma names.