Initial setup for code actions

This declares a code action provider that calls all @[hole_code_action] definitions on each occurrence of a hole (_, ?_ or sorry).

(This is in a separate file from Batteries.CodeAction.Hole.Attr so that the server does not attempt to use this code action provider when browsing the Batteries.CodeAction.Hole.Attr file itself.)

def Batteries.CodeAction.tacticCodeActionProvider : Lean.Server.CodeActionProvider

A code action which calls @[tactic_code_action] code actions.

Equations

• One or more equations did not get rendered due to their size.