mathlib documentation

core / init.meta.hole_command

meta structure hole_command  :

The front-end (e.g., Emacs, VS Code) can invoke commands for holes {! ... !} in a declaration. A command is a tactic that takes zero or more pre-terms in the hole, and returns a list of pair (s, descr) where 's' is a substitution and 'descr' is a short explanation for the substitution. Each string 's' represents a different way to fill the hole. The front-end is responsible for replacing the hole with the string/alternative selected by the user.

This infra-structure can be use to implement auto-fill and/or refine commands.

An action may return an empty list. This is useful for actions that just return information such as: the type of an expression, its normal form, etc.

meta def use_cmd  :