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

tactic.eqn_stub

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

lint_hole_cmd

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

tactic.list_constructors_hole

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

tactic.match_stub

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

tactic.instance_stub

Import using

import tactic.core
import tactic.basic

library_search

Invoking the hole command library_search ("Use library_search to complete the goal") calls the tactic library_search to produce a proof term with the type of the hole.

Running it on

example : 0 < 1 :=
{!!}

produces

example : 0 < 1 :=
nat.one_pos

Tags:

search
Try this

Related declarations

tactic.library_search_hole_cmd

Import using

import tactic.suggest
import tactic.basic

tidy

Invoking the hole command tidy ("Use tidy to complete the goal") runs the tactic of the same name, replacing the hole with the tactic script tidy produces.

Tags:

Related declarations

tactic.tidy_hole_cmd

Import using

import tactic.tidy
import tactic.basic