mathlib documentation

Hole commands

Hole commands

Both VS Code and emacs support integration for 'hole commands'.

In VS Code, if you enter {! !}, a small light bulb symbol will appear, and clicking on it gives a drop down menu of available hole commands. Running one of these will replace the {! !} with whatever text that hole command provides.

As of Lean 3.16.0c, hole commands can also be activated at underscores _.

In emacs, you can do something similar with C-c SPC.

Many of these commands are available whenever tactic.core is imported. Commands that require additional imports are noted below. All should be available with import tactic.

Equations Stub

Invoking hole command "Equations Stub" ("Generate a list of equations for a recursive definition") in the following:

meta def foo : {! expr  tactic unit !} -- `:=` is omitted

produces:

meta def foo : expr  tactic unit
| (expr.var a) := _
| (expr.sort a) := _
| (expr.const a a_1) := _
| (expr.mvar a a_1 a_2) := _
| (expr.local_const a a_1 a_2 a_3) := _
| (expr.app a a_1) := _
| (expr.lam a a_1 a_2 a_3) := _
| (expr.pi a a_1 a_2 a_3) := _
| (expr.elet a a_1 a_2 a_3) := _
| (expr.macro a a_1) := _

A similar result can be obtained by invoking "Equations Stub" on the following:

meta def foo : expr  tactic unit := -- do not forget to write `:=`!!
{! !}
meta def foo : expr  tactic unit := -- don't forget to erase `:=`!!
| (expr.var a) := _
| (expr.sort a) := _
| (expr.const a a_1) := _
| (expr.mvar a a_1 a_2) := _
| (expr.local_const a a_1 a_2 a_3) := _
| (expr.app a a_1) := _
| (expr.lam a a_1 a_2 a_3) := _
| (expr.pi a a_1 a_2 a_3) := _
| (expr.elet a a_1 a_2 a_3) := _
| (expr.macro a a_1) := _
Tags:
  • pattern matching
Related declarations
Import using
  • import tactic.core
  • import tactic.basic

Lint

Invoking the hole command lint ("Find common mistakes in current file") will print text that indicates mistakes made in the file above the command. It is equivalent to copying and pasting the output of #lint. On large files, it may take some time before the output appears.

Tags:
  • linting
Related declarations
Import using
  • import tactic.lint.frontend
  • import tactic.basic

List Constructors

This command lists the constructors that can be used to satisfy the expected type.

Invoking "List Constructors" ("Show the list of constructors of the expected type") in the following hole:

def foo :    :=
{! !}

produces:

def foo :    :=
{! sum.inl, sum.inr !}

and will display:

sum.inl :     

sum.inr :     
```
Tags:
  • goal information
Related declarations
Import using
  • import tactic.core
  • import tactic.basic

Match Stub

Hole command used to generate a match expression.

In the following:

meta def foo (e : expr) : tactic unit :=
{! e !}

invoking hole command "Match Stub" ("Generate a list of equations for a match expression") produces:

meta def foo (e : expr) : tactic unit :=
match e with
| (expr.var a) := _
| (expr.sort a) := _
| (expr.const a a_1) := _
| (expr.mvar a a_1 a_2) := _
| (expr.local_const a a_1 a_2 a_3) := _
| (expr.app a a_1) := _
| (expr.lam a a_1 a_2 a_3) := _
| (expr.pi a a_1 a_2 a_3) := _
| (expr.elet a a_1 a_2 a_3) := _
| (expr.macro a a_1) := _
end
Tags:
  • pattern matching
Related declarations
Import using
  • import tactic.core
  • import tactic.basic

instance_stub

Hole command used to fill in a structure's field when specifying an instance.

In the following:

instance : monad id :=
{! !}

invoking the hole command "Instance Stub" ("Generate a skeleton for the structure under construction.") produces:

instance : monad id :=
{ map := _,
  map_const := _,
  pure := _,
  seq := _,
  seq_left := _,
  seq_right := _,
  bind := _ }
Tags:
  • instances
Related declarations
Import using
  • import tactic.core
  • import tactic.basic