Given an expr α representing a type with numeral structure, of_nat α n creates the α-valued numeral expression corresponding to n.

Given an expr α representing a type with numeral structure, of_nat α n creates the α-valued numeral expression corresponding to n. The output is either a numeral or the negation of a numeral.

Generates an expression of the form ∃(args), inner. args is assumed to be a list of local constants. When possible, p ∧ q is used instead of ∃(_ : p), q.

traverse f e applies the monadic function f to the direct descendants of e.

mfoldl f a e folds the monadic function f over the subterms of the expression e, with initial value a.

get_result tac returns the result state of applying tac to the current state. Note that it does not update the current state.

of_tactic' tac lifts the tactic tac into the parser monad. This replaces of_tactic in core, which has a buggy implementation.

Override the builtin lean.parser.of_tactic coe, which is broken. (See test/tactics.lean for a failure case.)

emit_command_here str behaves as if the string str were placed as a user command at the current line.

emit_code_here str behaves as if the string str were placed at the current location in source code.

intercalate x [a, b, c] produces the format object a.x.b.x.c, where . represents format.join.

eval_expr' α e attempts to evaluate the expression e in the type α. This is a variant of eval_expr in core. Due to unexplained behavior in the VM, in rare situations the latter will fail but the former will succeed.

mk_fresh_name returns identifiers starting with underscores, which are not legal when emitted by tactic programs. mk_user_fresh_name turns the useful source of random names provided by mk_fresh_name into names which are usable by tactic programs.

The returned name has four components which are all strings.

has_attribute n n' checks whether n' has attribute n.

Checks whether the name is a simp lemma

Checks whether the name is an instance.

local_decls returns a dictionary mapping names to their corresponding declarations. Covers all declarations from the current file.

If {nm}_{n} doesn't exist in the environment, returns that, otherwise tries {nm}_{n+1}

Return a name which doesn't already exist in the environment. If nm doesn't exist, it returns that, otherwise it tries nm_2, nm_3, ...

Returns a pair (e, t), where e ← mk_const d.to_name, and t = d.type but with universe params updated to match the fresh universe metavariables in e.

This should have the same effect as just

do e ← mk_const d.to_name,
   t ← infer_type e,
   return (e, t)

but is hopefully faster.

mk_local n creates a dummy local variable with name n. The type of this local constant is a constant with name n, so it is very unlikely to be a meaningful expression.

local_def_value e returns the value of the expression e, assuming that e has been defined locally using a let expression. Otherwise it fails.

check_defn n e elaborates the pre-expression e, and succeeds if this is alpha-equivalent to the value of the declaration with name n.

pis loc_consts f is used to create a pi expression whose body is f. loc_consts should be a list of local constants. The function will abstract these local constants from f and bind them with pi binders.

For example, if a, b are local constants with types Ta, Tb, pis [a, b] `(f a b) will return the expression Π (a : Ta) (b : Tb), f a b

lambdas loc_consts f is used to create a lambda expression whose body is f. loc_consts should be a list of local constants. The function will abstract these local constants from f and bind them with lambda binders.

For example, if a, b are local constants with types Ta, Tb, lambdas [a, b] `(f a b) will return the expression λ (a : Ta) (b : Tb), f a b

Given elab_def, a tactic to solve the current goal, extract_def n trusted elab_def will create an auxiliary definition named n and use it to close the goal. If trusted is false, it will be a meta definition.

Attempts to close the goal with dec_trivial.

Runs a tactic for a result, reverting the state after completion

Repeat a tactic at least once, calling it recursively on all subgoals, until it fails. This tactic fails if the first invocation fails.

iterate_range m n t: Repeat the given tactic at least m times and at most n times or until t fails. Fails if t does not run at least m times.

Given a tactic tac that takes an expression and returns a new expression and a proof of equality, use that tactic to change the type of the hypotheses listed in hs, as well as the goal if tgt = tt.

Returns tt if any types were successfully changed.

A variant of simplify_bottom_up. Given a tactic post for rewriting subexpressions, simp_bottom_up post e tries to rewrite e starting at the leaf nodes. Returns the resulting expression and a proof of equality.

Caches unary type classes on a type α : Type.{univ}

Creates an instance_cache for the type α

If n is the name of a type class with one parameter, get c n tries to find an instance of n c.α by checking the cache c. If there is no entry in the cache, it tries to find the instance via type class resolution, and updates the cache.

If e is a pi expression that binds an instance-implicit variable of type n, append_typeclasses e c l searches c for an instance p of type n and returns p :: l.

Creates the application n c.α p l, where p is a type class instance found in the cache c.

Compute the arity of explicit arguments of the given (Pi-)type

Compute the arity of explicit arguments of the given function

Auxilliary defintion for get_pi_binders.

Get the binders and target of a pi-type. Instantiates bound variables by local constants. Cf. pi_binders in meta.expr (which produces open terms). See also mk_local_pis in init.core.tactic which does almost the same.

variation on assert where a (possibly incomplete) proof of the assertion is provided as a parameter.

(h,gs) ← local_proof `h p tac creates a local h : p and use tac to (partially) construct a proof for it. gs is the list of remaining goals in the proof of h.

The benefits over assert are:

• unlike with h ← assert `h p, tac , h cannot be used by tac;
• when tac does not complete the proof of h, returning the list of goals allows one to write a tactic using h and with the confidence that a proof will not boil over to goals left over from the proof of h, unlike what would be the case when using tactic.swap.

var_names e returns a list of the unique names of the initial pi bindings in e.

When struct_n is the name of a structure type, subobject_names struct_n returns two lists of names (instances, fields). The names in instances are the projections from struct_n to the structures that it extends (assuming it was defined with old_structure_cmd false). The names in fields are the standard fields of struct_n.

expanded_field_list struct_n produces a list of the names of the fields of the structure named struct_n. These are returned as pairs of names (prefix, name), where the full name of the projection is prefix.name.

Return a list of all type classes which can be instantiated for the given expression.

Create a list of n fresh metavariables.

Returns the only goal, or fails if there isn't just one goal.

iterate_at_most_on_all_goals n t: repeat the given tactic at most n times on all goals, or until it fails. Always succeeds.

iterate_at_most_on_subgoals n t: repeat the tactic t at most n times on the first goal and on all subgoals thus produced, or until it fails. Fails iff t fails on current goal.

apply_list l: try to apply the tactics in the list l on the first goal, and fail if none succeeds

constructs a list of expressions given a list of p-expressions, as follows:

• if the p-expression is the name of a theorem, use i_to_expr_for_apply on it
• if the p-expression is a user attribute, add all the theorems with this attribute to the list.

apply_rules hs n: apply the list of rules hs (given as pexpr) and assumption on the first goal and the resulting subgoals, iteratively, at most n times

replace h p elaborates the pexpr p, clears the existing hypothesis named h from the local context, and adds a new hypothesis named h. The type of this hypothesis is the type of p. Fails if there is nothing named h in the local context.

Auxiliary function for iff_mp and iff_mpr. Takes a name, which should be either `iff.mp or `iff.mpr. If the passed expression is an iterated function type eventually producing an iff, returns an expression with the iff converted to either the forwards or backwards implication, as requested.

iff_mp_core e ty assumes that ty is the type of e. If ty has the shape Π ..., A ↔ B, returns an expression whose type is Π ..., A → B

iff_mpr_core e ty assumes that ty is the type of e. If ty has the shape Π ..., A ↔ B, returns an expression whose type is Π ..., B → A

Given an expression whose type is (a possibly iterated function producing) an iff, create the expression which is the forward implication.

Given an expression whose type is (a possibly iterated function producing) an iff, create the expression which is the reverse implication.

Attempts to apply e, and if that fails, if e is an iff, try applying both directions separately.

symm_apply e cfg tries apply e cfg, and if this fails, calls symmetry and tries again.

apply_assumption searches for terms in the local context that can be applied to make progress on the goal. If the goal is symmetric, it tries each goal in both directions. If this fails, it will call exfalso and repeat. Optional arguments:

• asms controls which expressions are applied. Defaults to local_context
• tac is called after a successful application. Defaults to skip

change_core e none is equivalent to change e. It tries to change the goal to e and fails if this is not a definitional equality.

change_core e (some h) assumes h is a local constant, and tries to change the type of h to e by reverting h, changing the goal, and reintroducing hypotheses.

change_with_at olde newe hyp replaces occurences of olde with newe at hypothesis hyp, assuming olde and newe are defeq when elaborated.

Returns a list of all metavariables in the current partial proof. This can differ from the list of goals, since the goals can be manually edited.

Fail if the target contains a metavariable.

Succeeds only if the current goal is a proposition.

Succeeds only if we can construct an instance showing the current goal is a subsingleton type.

Succeeds only if the current goal is "terminal", in the sense that no other goals depend on it (except possibly through shared metavariables; see independent_goal).

Succeeds only if the current goal is "independent", in the sense that no other goals depend on it, even through shared meta-variables.

triv' tries to close the first goal with the proof trivial : true. Unlike triv, it only unfolds reducible definitions, so it sometimes fails faster.

Apply a tactic as many times as possible, collecting the results in a list.

Apply a tactic as many times as possible, collecting the results in a list. Fail if the tactic does not succeed at least once.

Introduces one or more variables and returns the new local constants. Fails if intro cannot be applied.

successes invokes each tactic in turn, returning the list of successful results.

Return target after instantiating metavars and whnf

Just like split, fsplit applies the constructor when the type of the target is an inductive data type with one constructor. However it does not reorder goals or invoke auto_param tactics.

Calls injection on each hypothesis, and then, for each hypothesis on which injection succeeds, clears the old hypothesis.

calls cases on every local hypothesis, succeeding if it succeeds on at least one hypothesis.

given a proof pr : t, adds h : t to the current context, where the name h is fresh.

find_local t returns a local constant with type t, or fails if none exists.

dependent_pose_core l: introduce dependent hypothesis, where the proofs depend on the values of the previous local constants. l is a list of local constants and their values.

like mk_local_pis but translating into weak head normal form before checking if it is a Π.

Changes (h : ∀xs, ∃a:α, p a) ⊢ g to (d : ∀xs, a) (s : ∀xs, p (d xs) ⊢ g

Changes (h : ∀xs, ∃as, p as) ⊢ g to a list of functions as, and a final hypothesis on p as

Instantiates metavariables that appear in the current goal.

Instantiates metavariables in all goals.

This makes sure that the execution of the tactic does not change the tactic state. This can be helpful while using rewrite, apply, or expr munging. Remember to instantiate your metavariables before you're done!

similar to mk_local_pis but make meta variables instead of local constants

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

In the following:

instance : monad id :=
{! !}

invoking hole command Instance Stub produces:

instance : monad id :=
{ map := _,
  map_const := _,
  pure := _,
  seq := _,
  seq_left := _,
  seq_right := _,
  bind := _ }

Like resolve_name except when the list of goals is empty. In that situation resolve_name fails whereas resolve_name' simply proceeds on a dummy goal

Strips unnecessary prefixes from a name, e.g. if a namespace is open.

Used to format return strings for the hole commands match_stub and eqn_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 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

Hole command used to generate a match expression.

In the following:

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

invoking hole command Equations Stub 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) := _

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

When used in the following hole:

def foo : ℤ ⊕ ℕ :=
{! !}

the command will produce:

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

and will display:

sum.inl : ℤ → ℤ ⊕ ℕ

sum.inr : ℕ → ℤ ⊕ ℕ

Makes the declaration classical.prop_decidable available to type class inference. This asserts that all propositions are decidable, but does not have computational content.

mk_comp v e checks whether e is a sequence of nested applications f (g (h v)), and if so, returns the expression f ∘ g ∘ h.

From a lemma of the shape ∀ x, f (g x) = h x derive an auxiliary lemma of the form f ∘ g = h for reasoning about higher-order functions.

A user attribute that applies to lemmas of the shape ∀ x, f (g x) = h x. It derives an auxiliary lemma of the form f ∘ g = h for reasoning about higher-order functions.

Use refine to partially discharge the goal, or call fconstructor and try again.

Similar to existsi, use l will use entries in l to instantiate existential obligations at the beginning of a target. Unlike existsi, the pexprs in l are elaborated with respect to the expected type.

example : ∃ x : ℤ, x = x :=
by tactic.use ``(42)

See the doc string for tactic.interactive.use for more information.

clear_aux_decl_aux l clears all expressions in l that represent aux decls from the local context.

clear_aux_decl clears all expressions from the local context that represent aux decls.

apply_at_aux e et [] h ht (with et the type of e and ht the type of h) finds a list of expressions vs and returns (e.mk_args (vs ++ [h]), vs)

apply_at e h applies implication e on hypothesis h and replaces h with the result

symmetry_hyp h applies symmetry on hypothesis h

setup_tactic_parser_cmd is a user command that opens the namespaces used in writing interactive tactics, and declares the local postfix notation ? for optional and * for many. It does not use the namespace command, so it will typically be used after namespace tactic.interactive.

trace_error msg t executes the tactic t. If t fails, traces msg and the failure message of t.

This combinator is for testing purposes. It succeeds if t fails with message msg, and fails otherwise.

A type alias for tactic format, standing for "pretty print format".

mk lifts fmt : format to the tactic monad (pformat).

an alias for pp.

See format! in init/meta/interactive_base.lean.

The main differences are that pp is called instead of to_fmt and that we can use arguments of type tactic α in the quotations.

Now, consider the following:

e ← to_expr ``(3 + 7),
trace format!"{e}"  -- outputs `has_add.add.{0} nat nat.has_add (bit1.{0} nat nat.has_one nat.has_add (has_one.one.{0} nat nat.has_one)) ...`
trace pformat!"{e}" -- outputs `3 + 7`

The difference is significant. And now, the following is expressible:

e ← to_expr ``(3 + 7),
trace pformat!"{e} : {infer_type e}" -- outputs `3 + 7 : ℕ`

See also: trace! and fail!

the combination of pformat and fail

the combination of pformat and fail

A hackish way to get the src directory of mathlib.

Checks whether a declaration with the given name is declared in mathlib. If you want to run this tactic many times, you should use environment.is_prefix_of_file instead, since it is expensive to execute get_mathlib_dir many times.

auxiliary function for apply_under_pis

Assumes pi_expr is of the form Π x1 ... xn, _. Creates a pexpr of the form Π x1 ... xn, func (arg x1 ... xn). All arguments (implicit and explicit) to arg should be supplied.

Tries to derive instances by unfolding the newly introduced type and applying type class resolution.

For example,

@[derive ring] def new_int : Type := ℤ

adds an instance ring new_int, defined to be the instance of ring ℤ found by apply_instance.

Multiple instances can be added with @[derive [ring, module ℝ]].

This derive handler applies only to declarations made using def, and will fail on such a declaration if it is unable to derive an instance. It is run with higher priority than the built-in handlers, which will fail on defs.

find_private_decl n none finds a private declaration named n in any of the imported files.

find_private_decl n (some m) finds a private declaration named n in the same file where a declaration named m can be found.

import_private foo from bar finds a private declaration foo in the same file as bar and creates a local notation to refer to it.

import_private foo, looks for foo in all imported files.