mathlib documentation

core / init.meta.tactic

source
meta constant tactic_state  :
Type
source
meta constant tactic_state.env  :
tactic_state → environment
source
meta constant tactic_state.to_format (s : tactic_state) (target_lhs_only : bool := ff) :
format

Format the given tactic state. If target_lhs_only is true and the target is of the form lhs ~ rhs, where ~ is a simplification relation, then only the lhs is displayed.

Remark: the parameter target_lhs_only is a temporary hack used to implement the conv monad. It will be removed in the future.

source
meta constant tactic_state.format_expr  :
tactic_state → expr → format

Format expression with respect to the main goal in the tactic state. If the tactic state does not contain any goals, then format expression using an empty local context.

source
meta constant tactic_state.get_options  :
tactic_state → options
source
meta constant tactic_state.set_options  :
tactic_state → options → tactic_state
source
@[protected, instance]
meta def tactic_state.has_to_format  :
has_to_format tactic_state
source
@[protected, instance]
meta def tactic_state.has_to_string  :
has_to_string tactic_state
source
meta def tactic (α : Type u_1) :
Type u_1

tactic is the monad for building tactics. You use this to:

  • View and modify the local goals and hypotheses in the prover's state.
  • Invoke type checking and elaboration of terms.
  • View and modify the environment.
  • Build new tactics out of existing ones such as simp and rewrite.
source
meta def tactic_result (α : Type u_1) :
Type u_1
source
meta def tactic.failed {α : Type} :
tactic α

Cause the tactic to fail with no error message.

source
meta def tactic.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) :
tactic α
source
@[protected, instance]
meta def tactic.alternative  :
alternative tactic
source
meta def tactic.up {α : Type u₂} (t : tactic α) :
tactic (ulift α)
source
meta def tactic.down {α : Type u₂} (t : tactic (ulift α)) :
tactic α
source
@[class]
meta structure interactive.executor (m : Type → Type u) [monad m] :
Type (max 1 u)

Typeclass for custom interaction monads, which provides the information required to convert an interactive-mode construction to a tactic which can actually be executed.

Given a [monad m], execute_with explains how to turn a begin ... end block, or a by ... statement into a tactic α which can actually be executed. The inhabited first argument facilitates the passing of an optional configuration parameter config, using the syntax:

begin [custom_monad] with config,
    ...
end
Instances
source
meta def interactive.executor.execute_explicit (m : Type → Type u) [monad m] [e : interactive.executor m] :
m unit → tactic unit
source
meta def interactive.executor.execute_with_explicit (m : Type → Type u) [monad m] [interactive.executor m] :
interactive.executor.config_type m → m unit → tactic unit
source
@[protected, instance]
meta def interactive.executor_tactic  :
interactive.executor tactic

Default executor instance for tactics themselves

source
meta def tactic.skip  :
tactic unit

Does nothing.

source
meta def tactic.try_core {α : Type u} (t : tactic α) :
tactic (option α)

try_core t acts like t, but succeeds even if t fails. It returns the result of t if t succeeded and none otherwise.

source
meta def tactic.try {α : Type u} (t : tactic α) :
tactic unit

try t acts like t, but succeeds even if t fails.

source
meta def tactic.try_lst  :
list (tactic unit) → tactic unit
source
meta def tactic.fail_if_success {α : Type u} (t : tactic α) :
tactic unit

fail_if_success t acts like t, but succeeds if t fails and fails if t succeeds. Changes made by t to the tactic_state are preserved only if t succeeds.

source
meta def tactic.success_if_fail {α : Type u} (t : tactic α) :
tactic unit

success_if_fail t acts like t, but succeeds if t fails and fails if t succeeds. Changes made by t to the tactic_state are preserved only if t succeeds.

source
meta def tactic.iterate_at_most {α : Type u} :
ℕ → tactic α → tactic (list α)

iterate_at_most n t iterates t n times or until t fails, returning the result of each successful iteration.

source
meta def tactic.iterate_at_most'  :
ℕ → tactic unit → tactic unit

iterate_at_most' n t repeats t n times or until t fails.

source
meta def tactic.iterate_exactly {α : Type u} :
ℕ → tactic α → tactic (list α)

iterate_exactly n t iterates t n times, returning the result of each iteration. If any iteration fails, the whole tactic fails.

source
meta def tactic.iterate_exactly'  :
ℕ → tactic unit → tactic unit

iterate_exactly' n t executes t n times. If any iteration fails, the whole tactic fails.

source
meta def tactic.iterate {α : Type u} :
tactic α → tactic (list α)

iterate t repeats t 100.000 times or until t fails, returning the result of each iteration.

source
meta def tactic.iterate'  :
tactic unit → tactic unit

iterate' t repeats t 100.000 times or until t fails.

source
meta def tactic.returnopt {α : Type u} (e : option α) :
tactic α
source
@[protected, instance]
meta def tactic.opt_to_tac {α : Type u} :
has_coe (option α) (tactic α)
source
meta def tactic.decorate_ex {α : Type u} (msg : format) (t : tactic α) :
tactic α

Decorate t's exceptions with msg.

source
meta def tactic.write (s' : tactic_state) :
tactic unit

Set the tactic_state.

source
meta def tactic.read  :
tactic tactic_state

Get the tactic_state.

source
meta def tactic.capture {α : Type u} (t : tactic α) :
tactic (tactic_result α)

capture t acts like t, but succeeds with a result containing either the returned value or the exception. Changes made by t to the tactic_state are preserved in both cases.

The result can be used to inspect the error message, or passed to unwrap to rethrow the failure later.

source
meta def tactic.unwrap {α : Type u_1} (t : tactic_result α) :
tactic α

unwrap r unwraps a result previously obtained using capture.

If the previous result was a success, this produces its wrapped value. If the previous result was an exception, this "rethrows" the exception as if it came from where it originated.

do r ← capture t, unwrap r is identical to t, but allows for intermediate tactics to be inserted.

source
meta def tactic.resume {α : Type u_1} (t : tactic_result α) :
tactic α

resume r continues execution from a result previously obtained using capture.

This is like unwrap, but the tactic_state is rolled back to point of capture even upon success.

source
meta def tactic.get_options  :
tactic options
source
meta def tactic.set_options (o : options) :
tactic unit
source
meta def tactic.save_options {α : Type} (t : tactic α) :
tactic α
source
meta def tactic.returnex {α : Type} (e : exceptional α) :
tactic α
source
@[protected, instance]
meta def tactic.ex_to_tac {α : Type} :
has_coe (exceptional α) (tactic α)
source
meta def tactic_format_expr (e : expr) :
tactic format
source
@[class]
meta structure has_to_tactic_format (α : Type u) :
Type u
Instances
source
@[protected, instance]
meta def expr.has_to_tactic_format  :
has_to_tactic_format expr
source
meta def tactic.pp {α : Type u} [has_to_tactic_format α] :
α → tactic format
source
@[protected, instance]
meta def list.has_to_tactic_format {α : Type u} [has_to_tactic_format α] :
has_to_tactic_format (list α)
source
@[protected, instance]
meta def prod.has_to_tactic_format (α : Type u) (β : Type v) [has_to_tactic_format α] [has_to_tactic_format β] :
has_to_tactic_format (α × β)
source
meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] :
option α → tactic format
source
@[protected, instance]
meta def option.has_to_tactic_format {α : Type u} [has_to_tactic_format α] :
has_to_tactic_format (option α)
source
@[protected, instance]
meta def reflected.has_to_tactic_format {α : Sort u_1} (a : α) :
has_to_tactic_format (reflected a)
source
@[protected, instance]
meta def has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] :
has_to_tactic_format α
source
meta def tactic.get_env  :
tactic environment
source
meta def tactic.get_decl (n : name) :
tactic declaration
source
meta constant tactic.get_trace_msg_pos  :
tactic pos
source
meta def tactic.trace {α : Type u} [has_to_tactic_format α] (a : α) :
tactic unit
source
meta def tactic.trace_call_stack  :
tactic unit
source
meta def tactic.timetac {α : Type u} (desc : string) (t : thunk (tactic α)) :
tactic α
source
meta def tactic.trace_state  :
tactic unit
source
inductive tactic.transparency  :
Type

A parameter representing how aggressively definitions should be unfolded when trying to decide if two terms match, unify or are definitionally equal. By default, theorem declarations are never unfolded.

  • all will unfold everything, including macros and theorems. Except projection macros.
  • semireducible will unfold everything except theorems and definitions tagged as irreducible.
  • instances will unfold all class instance definitions and definitions tagged with reducible.
  • reducible will only unfold definitions tagged with the reducible attribute.
  • none will never unfold anything. [NOTE] You are not allowed to tag a definition with more than one of reducible, irreducible, semireducible attributes. [NOTE] there is a config flag m_unfold_lemmasthat will make it unfold theorems.
source
meta constant tactic.eval_expr (α : Type u) [reflected α] :
expr → tactic α

(eval_expr α e) evaluates 'e' IF 'e' has type 'α'.

source
meta constant tactic.result  :
tactic expr

Return the partial term/proof constructed so far. Note that the resultant expression may contain variables that are not declarate in the current main goal.

source
meta constant tactic.format_result  :
tactic format

Display the partial term/proof constructed so far. This tactic is not equivalent to do { r ← result, s ← read, return (format_expr s r) } because this one will format the result with respect to the current goal, and trace_result will do it with respect to the initial goal.

source
meta constant tactic.target  :
tactic expr

Return target type of the main goal. Fail if tactic_state does not have any goal left.

source
meta constant tactic.intro_core  :
name → tactic expr
source
meta constant tactic.intron  :
ℕ → tactic unit
source
meta constant tactic.clear  :
expr → tactic unit

Clear the given local constant. The tactic fails if the given expression is not a local constant.

source
meta constant tactic.revert_lst  :
list expr → tactic ℕ

revert_lst : list expr → tactic nat is the reverse of intron. It takes a local constant c and puts it back as bound by a pi or elet of the main target. If there are other local constants that depend on c, these are also reverted. Because of this, the nat that is returned is the actual number of reverted local constants. Example: with x : ℕ, h : P(x) ⊢ T(x), revert_lst [x] returns 2 and produces the state ⊢ Π x, P(x) → T(x).

source
meta constant tactic.whnf (e : expr) (md : tactic.transparency := semireducible) (unfold_ginductive : bool := tt) :
tactic expr

Return e in weak head normal form with respect to the given transparency setting. If unfold_ginductive is tt, then nested and/or mutually recursive inductive datatype constructors and types are unfolded. Recall that nested and mutually recursive inductive datatype declarations are compiled into primitive datatypes accepted by the Kernel.

source
meta constant tactic.head_eta_expand  :
expr → tactic expr

(head) eta expand the given expression. f : α → β head-eta-expands to λ a, f a. If f isn't a function then it just returns f.

source
meta constant tactic.head_beta  :
expr → tactic expr

(head) beta reduction. (λ x, B) c reduces to B[x/c].

source
meta constant tactic.head_zeta  :
expr → tactic expr

(head) zeta reduction. Reduction of let bindings at the head of the expression. let x : a := b in c reduces to c[x/b].

source
meta constant tactic.zeta  :
expr → tactic expr

Zeta reduction. Reduction of let bindings. let x : a := b in c reduces to c[x/b].

source
meta constant tactic.head_eta  :
expr → tactic expr

(head) eta reduction. (λ x, f x) reduces to f.

source
meta constant tactic.unify (t s : expr) (md : tactic.transparency := semireducible) (approx : bool := ff) :
tactic unit

Succeeds if t and s can be unified using the given transparency setting.

source
meta constant tactic.is_def_eq (t s : expr) (md : tactic.transparency := semireducible) (approx : bool := ff) :
tactic unit

Similar to unify, but it treats metavariables as constants.

source
meta constant tactic.infer_type  :
expr → tactic expr

Infer the type of the given expression. Remark: transparency does not affect type inference

source
meta constant tactic.get_local  :
name → tactic expr

Get the local_const expr for the given name.

source
meta constant tactic.resolve_name  :
name → tactic pexpr

Resolve a name using the current local context, environment, aliases, etc.

source
meta constant tactic.local_context  :
tactic (list expr)

Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left.

source
meta constant tactic.get_unused_name (n : name := name.mk_string "_x" name.anonymous) (i : option ℕ := none) :
tactic name

Get a fresh name that is guaranteed to not be in use in the local context. If n is provided and n is not in use, then n is returned. Otherwise a number i is appended to give "n_i".

source
meta constant tactic.mk_app (fn : name) (args : list expr) (md : tactic.transparency := semireducible) :
tactic expr

Helper tactic for creating simple applications where some arguments are inferred using type inference.

Example, given

    rel.{l_1 l_2} : Pi (α : Type.{l_1}) (β : α -> Type.{l_2}), (Pi x : α, β x) -> (Pi x : α, β x) -> , Prop
    nat     : Type
    real    : Type
    vec.{l} : Pi (α : Type l) (n : nat), Type.{l1}
    f g     : Pi (n : nat), vec real n

then

mk_app_core semireducible "rel" [f, g]

returns the application

rel.{1 2} nat (fun n : nat, vec real n) f g

The unification constraints due to type inference are solved using the transparency md.

source
meta constant tactic.mk_mapp (fn : name) (args : list (option expr)) (md : tactic.transparency := semireducible) :
tactic expr

Similar to mk_app, but allows to specify which arguments are explicit/implicit. Example, given (a b : nat) then

mk_mapp "ite" [some (a > b), none, none, some a, some b]

returns the application

@ite.{1} nat (a > b) (nat.decidable_gt a b) a b
source
meta constant tactic.mk_congr_arg  :
expr → expr → tactic expr

(mk_congr_arg h₁ h₂) is a more efficient version of (mk_app `congr_arg [h₁, h₂])

source
meta constant tactic.mk_congr_fun  :
expr → expr → tactic expr

(mk_congr_fun h₁ h₂) is a more efficient version of (mk_app `congr_fun [h₁, h₂])

source
meta constant tactic.mk_congr  :
expr → expr → tactic expr

(mk_congr h₁ h₂) is a more efficient version of (mk_app `congr [h₁, h₂])

source
meta constant tactic.mk_eq_refl  :
expr → tactic expr

(mk_eq_refl h) is a more efficient version of (mk_app `eq.refl [h])

source
meta constant tactic.mk_eq_symm  :
expr → tactic expr

(mk_eq_symm h) is a more efficient version of (mk_app `eq.symm [h])

source
meta constant tactic.mk_eq_trans  :
expr → expr → tactic expr

(mk_eq_trans h₁ h₂) is a more efficient version of (mk_app `eq.trans [h₁, h₂])

source
meta constant tactic.mk_eq_mp  :
expr → expr → tactic expr

(mk_eq_mp h₁ h₂) is a more efficient version of (mk_app `eq.mp [h₁, h₂])

source
meta constant tactic.mk_eq_mpr  :
expr → expr → tactic expr

(mk_eq_mpr h₁ h₂) is a more efficient version of (mk_app `eq.mpr [h₁, h₂])

source
meta constant tactic.subst_core  :
expr → tactic unit

Given a local constant t, if t has type (lhs = rhs) apply substitution. Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t). The tactic fails if the given expression is not a local constant.

source
meta constant tactic.exact (e : expr) (md : tactic.transparency := semireducible) :
tactic unit

Close the current goal using e. Fail if the type of e is not definitionally equal to the target type.

source
meta constant tactic.to_expr (q : pexpr) (allow_mvars subgoals : bool := tt) :
tactic expr

Elaborate the given quoted expression with respect to the current main goal. Note that this means that any implicit arguments for the given pexpr will be applied with fresh metavariables. If allow_mvars is tt, then metavariables are tolerated and become new goals if subgoals is tt.

source
meta constant tactic.is_class  :
expr → tactic bool

Return true if the given expression is a type class.

source
meta constant tactic.mk_instance  :
expr → tactic expr

Try to create an instance of the given type class.

source
meta constant tactic.change (e : expr) (check : bool := tt) :
tactic unit

Change the target of the main goal. The input expression must be definitionally equal to the current target. If check is ff, then the tactic does not check whether e is definitionally equal to the current target. If it is not, then the error will only be detected by the kernel type checker.

source
meta constant tactic.assert_core  :
name → expr → tactic unit

assert_core H T, adds a new goal for T, and change target to T -> target.

source
meta constant tactic.assertv_core  :
name → expr → expr → tactic unit

assertv_core H T P, change target to (T -> target) if P has type T.

source
meta constant tactic.define_core  :
name → expr → tactic unit

define_core H T, adds a new goal for T, and change target to let H : T := ?M in target in the current goal.

source
meta constant tactic.definev_core  :
name → expr → expr → tactic unit

definev_core H T P, change target to let H : T := P in target if P has type T.

source
meta constant tactic.rotate_left  :
ℕ → tactic unit

Rotate goals to the left. That is, rotate_left 1 takes the main goal and puts it to the back of the subgoal list.

source
meta constant tactic.get_goals  :
tactic (list expr)

Gets a list of metavariables, one for each goal.

source
meta constant tactic.set_goals  :
list expr → tactic unit

Replace the current list of goals with the given one. Each expr in the list should be a metavariable. Any assigned metavariables will be ignored.

source
inductive tactic.new_goals  :
Type

How to order the new goals made from an apply tactic. Supposing we were applying e : ∀ (a:α) (p : P(a)), Q

  • non_dep_first would produce goals ⊢ P(?m), ⊢ α. It puts the P goal at the front because none of the arguments after p in e depend on p. It doesn't matter what the result Q depends on.
  • non_dep_only would produce goal ⊢ P(?m).
  • all would produce goals ⊢ α, ⊢ P(?m).
source
structure tactic.apply_cfg  :
Type

Configuration options for the apply tactic.

  • md sets how aggressively definitions are unfolded.
  • new_goals is the strategy for ordering new goals.
  • instances if tt, then apply tries to synthesize unresolved [...] arguments using type class resolution.
  • auto_param if tt, then apply tries to synthesize unresolved (h : p . tac_id) arguments using tactic tac_id.
  • opt_param if tt, then apply tries to synthesize unresolved (a : t := v) arguments by setting them to v.
  • unify if tt, then apply is free to assign existing metavariables in the goal when solving unification constraints. For example, in the goal |- ?x < succ 0, the tactic apply succ_lt_succ succeeds with the default configuration, but apply_with succ_lt_succ {unify := ff} doesn't since it would require Lean to assign ?x to succ ?y where ?y is a fresh metavariable.
source
meta constant tactic.apply_core (e : expr) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :
tactic (list (name × expr))

Apply the expression e to the main goal, the unification is performed using the transparency mode in cfg. Supposing e : Π (a₁:α₁) ... (aₙ:αₙ), P(a₁,...,aₙ) and the target is Q, apply will attempt to unify Q with P(?a₁,...?aₙ). All of the metavariables that are not assigned are added as new metavariables. If cfg.approx is tt, then fallback to first-order unification, and approximate context during unification. cfg.new_goals specifies which unassigned metavariables become new goals, and their order. If cfg.instances is tt, then use type class resolution to instantiate unassigned meta-variables. The fields cfg.auto_param and cfg.opt_param are ignored by this tactic (See tactic.apply). It returns a list of all introduced meta variables and the parameter name associated with them, even the assigned ones.

source
meta constant tactic.mk_meta_univ  :
tactic level
source
meta constant tactic.mk_meta_var  :
expr → tactic expr
source
meta constant tactic.get_univ_assignment  :
level → tactic level

Return the value assigned to the given universe meta-variable. Fail if argument is not an universe meta-variable or if it is not assigned.

source
meta constant tactic.get_assignment  :
expr → tactic expr

Return the value assigned to the given meta-variable. Fail if argument is not a meta-variable or if it is not assigned.

source
meta constant tactic.is_assigned  :
expr → tactic bool

Return true if the given meta-variable is assigned. Fail if argument is not a meta-variable.

source
meta constant tactic.mk_fresh_name  :
tactic name

Make a name that is guaranteed to be unique. Eg _fresh.1001.4667. These will be different for each run of the tactic.

source
meta constant tactic.induction (h : expr) (ns : list name := list.nil) (rec : option name := none) (md : tactic.transparency := semireducible) :
tactic (list (name × list expr × list (name × expr)))

Induction on h using recursor rec, names for the new hypotheses are retrieved from ns. If ns does not have sufficient names, then use the internal binder names in the recursor. It returns for each new goal the name of the constructor (if rec_name is a builtin recursor), a list of new hypotheses, and a list of substitutions for hypotheses depending on h. The substitutions map internal names to their replacement terms. If the replacement is again a hypothesis the user name stays the same. The internal names are only valid in the original goal, not in the type context of the new goal. Remark: if rec_name is not a builtin recursor, we use parameter names of rec_name instead of constructor names.

If rec is none, then the type of h is inferred, if it is of the form C ..., tactic uses C.rec

source
meta constant tactic.cases_core (h : expr) (ns : list name := list.nil) (md : tactic.transparency := semireducible) :
tactic (list (name × list expr × list (name × expr)))

Apply cases_on recursor, names for the new hypotheses are retrieved from ns. h must be a local constant. It returns for each new goal the name of the constructor, a list of new hypotheses, and a list of substitutions for hypotheses depending on h. The number of new goals may be smaller than the number of constructors. Some goals may be discarded when the indices to not match. See induction for information on the list of substitutions.

The cases tactic is implemented using this one, and it relaxes the restriction of h.

Note: There is one "new hypothesis" for every constructor argument. These are usually local constants, but due to dependent pattern matching, they can also be arbitrary terms.

source
meta constant tactic.destruct (e : expr) (md : tactic.transparency := semireducible) :
tactic unit

Similar to cases tactic, but does not revert/intro/clear hypotheses.

source
meta constant tactic.generalize (e : expr) (n : name := name.mk_string "_x" name.anonymous) (md : tactic.transparency := semireducible) :
tactic unit

Generalizes the target with respect to e.

source
meta constant tactic.instantiate_mvars  :
expr → tactic expr

instantiate assigned metavariables in the given expression

source
meta constant tactic.add_decl  :
declaration → tactic unit

Add the given declaration to the environment

source
meta constant tactic.set_env_core  :
environment → tactic unit

Changes the environment to the new_env. The new environment does not need to be a descendant of the old one. Use with care.

source
meta constant tactic.set_env  :
environment → tactic unit

Changes the environment to the new_env. new_env needs to be a descendant from the current environment.

source
meta constant tactic.doc_string  :
name → tactic string

doc_string env d k returns the doc string for d (if available)

source
meta constant tactic.add_doc_string  :
name → string → tactic unit

Set the docstring for the given declaration.

source
meta constant tactic.add_aux_decl (c : name) (type val : expr) (is_lemma : bool) :
tactic expr

Create an auxiliary definition with name c where type and value may contain local constants and meta-variables. This function collects all dependencies (universe parameters, universe metavariables, local constants (aka hypotheses) and metavariables). It updates the environment in the tactic_state, and returns an expression of the form

      (c.{l_1 ... l_n} a_1 ... a_m)

where l_i's and a_j's are the collected dependencies.

source
meta constant tactic.olean_doc_strings  :
tactic (list (option string × list (pos × string)))

Returns a list of all top-level (/-! ... -/) docstrings in the active module and imported ones. The returned object is a list of modules, indexed by (some filename) for imported modules and none for the active one, where each module in the list is paired with a list of (position_in_file, docstring) pairs.

source
meta def tactic.module_doc_strings  :
tactic (list (option name × string))

Returns a list of docstrings in the active module. An entry in the list can be either:

  • a top-level (/-! ... -/) docstring, represented as (none, docstring)
  • a declaration-specific (/-- ... -/) docstring, represented as (some decl_name, docstring)
source
meta constant tactic.set_basic_attribute (attr_name c_name : name) (persistent : bool := ff) (prio : option ℕ := none) :
tactic unit

Set attribute attr_name for constant c_name with the given priority. If the priority is none, then use default

source
meta constant tactic.unset_attribute  :
name → name → tactic unit

unset_attribute attr_name c_name

source
meta constant tactic.has_attribute  :
name → name → tactic (bool × ℕ)

has_attribute attr_name c_name succeeds if the declaration decl_name has the attribute attr_name. The result is the priority and whether or not the attribute is persistent.

source
meta def tactic.copy_attribute (attr_name src tgt : name) (p : option bool := none) :
tactic unit

copy_attribute attr_name c_name p d_name copy attribute attr_name from src to tgt if it is defined for src; make it persistent if p is tt; if p is none, the copied attribute is made persistent iff it is persistent on src

source
meta constant tactic.decl_name  :
tactic name

Name of the declaration currently being elaborated.

source
meta constant tactic.save_type_info {elab : bool} :
expr → expr elab → tactic unit

save_type_info e ref save (typeof e) at position associated with ref

source
meta constant tactic.save_info_thunk  :
pos → (unit → format) → tactic unit
source
meta constant tactic.open_namespaces  :
tactic (list name)

Return list of currently open namespaces

source
meta constant tactic.kdepends_on (e t : expr) (md : tactic.transparency := reducible) :
tactic bool

Return tt iff t "occurs" in e. The occurrence checking is performed using keyed matching with the given transparency setting.

We say t occurs in e by keyed matching iff there is a subterm s s.t. t and s have the same head, and is_def_eq t s md

The main idea is to minimize the number of is_def_eq checks performed.

source
meta constant tactic.kabstract (e t : expr) (md : tactic.transparency := reducible) (unify : bool := tt) :
tactic expr

Abstracts all occurrences of the term t in e using keyed matching. If unify is ff, then matching is used instead of unification. That is, metavariables occurring in e are not assigned.

source
meta constant tactic.sleep (msecs : ℕ) :
tactic unit

Blocks the execution of the current thread for at least msecs milliseconds. This tactic is used mainly for debugging purposes.

source
meta constant tactic.type_check (e : expr) (md : tactic.transparency := semireducible) :
tactic unit

Type check e with respect to the current goal. Fails if e is not type correct.

source
def tactic.tag  :
Type

A tag is a list of names. These are attached to goals to help tactics track them.

Equations
source
meta constant tactic.enable_tags (b : bool) :
tactic unit

Enable/disable goal tagging.

source
meta constant tactic.tags_enabled  :
tactic bool

Return tt iff goal tagging is enabled.

source
meta constant tactic.set_tag (g : expr) (t : tactic.tag) :
tactic unit

Tag goal g with tag t. It does nothing if goal tagging is disabled. Remark: set_goal g [] removes the tag

source
meta constant tactic.get_tag (g : expr) :
tactic tactic.tag

Return tag associated with g. Return [] if there is no tag.

source
meta constant tactic.unfreeze_local_instances  :
tactic unit

By default, Lean only considers local instances in the header of declarations. This has two main benefits. 1- Results produced by the type class resolution procedure can be easily cached. 2- The set of local instances does not have to be recomputed.

This approach has the following disadvantages: 1- Frozen local instances cannot be reverted. 2- Local instances defined inside of a declaration are not considered during type class resolution.

This tactic resets the set of local instances. After executing this tactic, the set of local instances will be recomputed and the cache will be frequently reset. Note that, the cache is still used when executing a single tactic that may generate many type class resolution problems (e.g., simp).

source
meta constant tactic.freeze_local_instances  :
tactic unit

Freeze the current set of local instances.

source
meta constant tactic.frozen_local_instances  :
tactic (option (list expr))
source
meta constant tactic.with_ast {α : Type u} (ast : ℕ) (t : tactic α) :
tactic α

Run the provided tactic, associating it to the given AST node.

source
meta def tactic.induction' (h : expr) (ns : list name := list.nil) (rec : option name := none) (md : tactic.transparency := semireducible) :
tactic unit
source
meta def tactic.cleanup  :
tactic unit

Remark: set_goals will erase any solved goal

source
meta def tactic.step {α : Type u} (t : tactic α) :
tactic unit

Auxiliary definition used to implement begin ... end blocks

source
meta def tactic.istep {α : Type u} (line0 col0 line col ast : ℕ) (t : tactic α) :
tactic unit
source
meta def tactic.is_prop (e : expr) :
tactic bool
source
meta def tactic.is_prop_decl (n : name) :
tactic bool

Return true iff n is the name of declaration that is a proposition.

source
meta def tactic.is_proof (e : expr) :
tactic bool
source
meta def tactic.whnf_no_delta (e : expr) :
tactic expr
source
meta def tactic.whnf_ginductive (e : expr) (md : tactic.transparency := semireducible) :
tactic expr

Return e in weak head normal form with respect to the given transparency setting, or e head is a generalized constructor or inductive datatype.

source
meta def tactic.whnf_target  :
tactic unit
source
meta def tactic.unsafe_change (e : expr) :
tactic unit

Change the target of the main goal. The input expression must be definitionally equal to the current target. The tactic does not check whether e is definitionally equal to the current target. The error will only be detected by the kernel type checker.

source
meta def tactic.intro (n : name) :
tactic expr

Pi or elet introduction. Given the tactic state ⊢ Π x : α, Y, intro `hello will produce the state hello : α ⊢ Y[x/hello]. Returns the new local constant. Similarly for elet expressions. If the target is not a Pi or elet it will try to put it in WHNF.

source
meta def tactic.intro_fresh (n : name) (offset : option ℕ := none) :
tactic expr

A variant of intro which makes sure that the introduced hypothesis's name is unique in the context. If there is no hypothesis named n in the context yet, intro_fresh n is the same as intro n. If there is already a hypothesis named n, the new hypothesis is named n_1 (or n_2 if n_1 already exists, etc.). If offset is given, the new names are n_offset, n_offset+1 etc.

If n is _, intro_fresh n is the same as intro1. The offset is ignored in this case.

source
meta def tactic.intro1  :
tactic expr

Like intro except the name is derived from the bound name in the Π.

source
meta def tactic.intros  :
tactic (list expr)

Repeatedly apply intro1 and return the list of new local constants in order of introduction.

source
meta def tactic.intro_lst (ns : list name) :
tactic (list expr)

Same as intros, except with the given names for the new hypotheses. Use the name _ to instead use the binder's name.

source
meta def tactic.intro_lst_fresh (ns : list name) :
tactic (list expr)

A variant of intro_lst which makes sure that the introduced hypotheses' names are unique in the context. See intro_fresh.

source
meta def tactic.intros_dep  :
tactic (list expr)

Introduces new hypotheses with forward dependencies.

source
meta def tactic.introv  :
list name → tactic (list expr)
source
meta def tactic.intron' (n : ℕ) :
tactic (list expr)

intron' n introduces n hypotheses and returns the resulting local constants. Fails if there are not at least n arguments to introduce. If you do not need the return value, use intron.

source
meta def tactic.intron_base (n : ℕ) (base : name) (offset : option ℕ := none) :
tactic (list expr)

Like intron' but the introduced hypotheses' names are derived from base, i.e. base, base_1 etc. The new names are unique in the context. If offset is given, the new names will be base_offset, base_offset+1 etc.

source
meta def tactic.intron_with  :
ℕ → list name → (name := name.mk_string "_" name.anonymous) → (option ℕ := none) → tactic (list expr × list name)

intron_with i ns base offset introduces i hypotheses using the names from ns. If ns contains less than i names, the remaining hypotheses' names are derived from base and offset (as with intron_base). If base is _, the names are derived from the Π binder names.

Returns the introduced local constants and the remaining names from ns (if ns contains more than i names).

source
meta def tactic.resolve_constant (n : name) :
tactic name

Returns n fully qualified if it refers to a constant, or else fails.

source
meta def tactic.to_expr_strict (q : pexpr) :
tactic expr
source
meta def tactic.revert (l : expr) :
tactic ℕ

Example: with x : ℕ, h : P(x) ⊢ T(x), revert x returns 2 and produces the state ⊢ Π x, P(x) → T(x).

source
meta def tactic.revert_all  :
tactic ℕ
source
meta def tactic.clear_lst  :
list name → tactic unit
source
meta def tactic.match_not (e : expr) :
tactic expr
source
meta def tactic.match_and (e : expr) :
tactic (expr × expr)
source
meta def tactic.match_or (e : expr) :
tactic (expr × expr)
source
meta def tactic.match_iff (e : expr) :
tactic (expr × expr)
source
meta def tactic.match_eq (e : expr) :
tactic (expr × expr)
source
meta def tactic.match_ne (e : expr) :
tactic (expr × expr)
source
meta def tactic.match_heq (e : expr) :
tactic (expr × expr × expr × expr)
source
meta def tactic.match_refl_app (e : expr) :
tactic (name × expr × expr)
source
meta def tactic.match_app_of (e : expr) (n : name) :
tactic (list expr)
source
meta def tactic.get_local_type (n : name) :
tactic expr
source
meta def tactic.trace_result  :
tactic unit
source
meta def tactic.rexact (e : expr) :
tactic unit
source
meta def tactic.any_hyp_aux {α : Type} (f : expr → tactic α) :
list expr → tactic α
source
meta def tactic.any_hyp {α : Type} (f : expr → tactic α) :
tactic α
source
meta def tactic.find_same_type  :
expr → list expr → tactic expr

find_same_type t es tries to find in es an expression with type definitionally equal to t

source
meta def tactic.find_assumption (e : expr) :
tactic expr
source
meta def tactic.assumption  :
tactic unit
source
meta def tactic.save_info (p : pos) :
tactic unit
source
meta def tactic.swap  :
tactic unit

Swap first two goals, do nothing if tactic state does not have at least two goals.

source
meta def tactic.assert (h : name) (t : expr) :
tactic expr

assert h t, adds a new goal for t, and the hypothesis h : t in the current goal.

source
meta def tactic.assertv (h : name) (t v : expr) :
tactic expr

assertv h t v, adds the hypothesis h : t in the current goal if v has type t.

source
meta def tactic.define (h : name) (t : expr) :
tactic expr

define h t, adds a new goal for t, and the hypothesis h : t := ?M in the current goal.

source
meta def tactic.definev (h : name) (t v : expr) :
tactic expr

definev h t v, adds the hypothesis (h : t := v) in the current goal if v has type t.

source
meta def tactic.pose (h : name) (t : option expr := none) (pr : expr) :
tactic expr

Add h : t := pr to the current goal

source
meta def tactic.note (h : name) (t : option expr := none) (pr : expr) :
tactic expr

Add h : t to the current goal, given a proof pr : t

source
meta def tactic.num_goals  :
tactic ℕ

Return the number of goals that need to be solved

source
meta def tactic.rotate_right (n : ℕ) [has_mod ℕ] :
tactic unit

Rotate the goals to the right by n. That is, take the goal at the back and push it to the front n times. [NOTE] We have to provide the instance argument [has_mod nat] because mod for nat was not defined yet

source
meta def tactic.rotate  :
ℕ → tactic unit

Rotate the goals to the left by n. That is, put the main goal to the back n times.

source
meta def tactic.repeat (t : tactic unit) :
tactic unit

This tactic is applied to each goal. If the application succeeds, the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed to make progress. The tactic repeat never fails.

source
meta def tactic.first {α : Type u} :
list (tactic α) → tactic α

first [t_1, ..., t_n] applies the first tactic that doesn't fail. The tactic fails if all t_i's fail.

source
meta def tactic.solve1 {α : Type} (tac : tactic α) :
tactic α

Applies the given tactic to the main goal and fails if it is not solved.

source
meta def tactic.solve {α : Type} (ts : list (tactic α)) :
tactic α

solve [t_1, ... t_n] applies the first tactic that solves the main goal.

source
meta def tactic.focus {α : Type} (ts : list (tactic α)) :
tactic (list α)

focus [t_1, ..., t_n] applies t_i to the i-th goal. Fails if the number of goals is not n. Returns the results of t_i (one per goal).

source
meta def tactic.focus' (ts : list (tactic unit)) :
tactic unit

focus' [t_1, ..., t_n] applies t_i to the i-th goal. Fails if the number of goals is not n.

source
meta def tactic.focus1 {α : Type} (tac : tactic α) :
tactic α
source
meta def tactic.all_goals {α : Type} (tac : tactic α) :
tactic (list α)

Apply the given tactic to all goals. Return one result per goal.

source
meta def tactic.all_goals' (tac : tactic unit) :
tactic unit

Apply the given tactic to all goals.

source
meta def tactic.any_goals {α : Type} (tac : tactic α) :
tactic (list (option α))

Apply tac to any goal where it succeeds. The tactic succeeds if tac succeeds for at least one goal. The returned list contains the result of tac for each goal: some a if tac succeeded, or none if it did not.

source
meta def tactic.any_goals' (tac : tactic unit) :
tactic unit

Apply the given tactic to any goal where it succeeds. The tactic succeeds only if tac succeeds for at least one goal.

source
meta def tactic.seq {α β : Type} (tac1 : tactic α) (tac2 : α → tactic β) :
tactic (list β)

LCF-style AND_THEN tactic. It applies tac1 to the main goal, then applies tac2 to each goal produced by tac1.

source
meta def tactic.seq' (tac1 tac2 : tactic unit) :
tactic unit

LCF-style AND_THEN tactic. It applies tac1, and if succeed applies tac2 to each subgoal produced by tac1

source
meta def tactic.seq_focus {α β : Type} (tac1 : tactic α) (tacs2 : α → list (tactic β)) :
tactic (list β)

Applies tac1 to the main goal, then applies each of the tactics in tacs2 to one of the produced subgoals (like focus').

source
meta def tactic.seq_focus' (tac1 : tactic unit) (tacs2 : list (tactic unit)) :
tactic unit

Applies tac1 to the main goal, then applies each of the tactics in tacs2 to one of the produced subgoals (like focus).

source
@[protected, instance]
meta def tactic.andthen_seq  :
has_andthen (tactic unit) (tactic unit) (tactic unit)
source
@[protected, instance]
meta def tactic.andthen_seq_focus  :
has_andthen (tactic unit) (list (tactic unit)) (tactic unit)
source
meta constant tactic.is_trace_enabled_for  :
name → bool
source
meta def tactic.when_tracing (n : name) (tac : tactic unit) :
tactic unit

Execute tac only if option trace.n is set to true.

source
meta def tactic.fail_if_no_goals  :
tactic unit

Fail if there are no remaining goals.

source
meta def tactic.done  :
tactic unit

Fail if there are unsolved goals.

source
meta def tactic.apply_opt_param  :
tactic unit
source
meta def tactic.apply_auto_param  :
tactic unit
source
meta def tactic.has_opt_auto_param (ms : list expr) :
tactic bool
source
meta def tactic.try_apply_opt_auto_param (cfg : tactic.apply_cfg) (ms : list expr) :
tactic unit
source
meta def tactic.has_opt_auto_param_for_apply (ms : list (name × expr)) :
tactic bool
source
meta def tactic.try_apply_opt_auto_param_for_apply (cfg : tactic.apply_cfg) (ms : list (name × expr)) :
tactic unit
source
meta def tactic.apply (e : expr) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :
tactic (list (name × expr))
source
meta def tactic.fapply (e : expr) :
tactic (list (name × expr))

Same as apply but all arguments that weren't inferred are added to goal list.

source
meta def tactic.eapply (e : expr) :
tactic (list (name × expr))

Same as apply but only goals that don't depend on other goals are added to goal list.

source
meta def tactic.apply_instance  :
tactic unit

Try to solve the main goal using type class resolution.

source
meta def tactic.mk_num_meta_univs  :
ℕ → tactic (list level)

Create a list of universe meta-variables of the given size.

source
meta def tactic.mk_const (c : name) :
tactic expr

Return expr.const c [l_1, ..., l_n] where l_i's are fresh universe meta-variables.

source
meta def tactic.applyc (c : name) (cfg : tactic.apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}) :
tactic unit

Apply the constant c

source
meta def tactic.eapplyc (c : name) :
tactic unit
source
meta def tactic.save_const_type_info (n : name) {elab : bool} (ref : expr elab) :
tactic unit
source
meta def tactic.mk_mvar  :
tactic expr

Create a fresh universe ?u, a metavariable ?T : Type.{?u}, and return metavariable ?M : ?T. This action can be used to create a meta-variable when we don't know its type at creation time

source
meta def tactic.mk_sorry  :
tactic expr

Makes a sorry macro with a meta-variable as its type.

source
meta def tactic.admit  :
tactic unit

Closes the main goal using sorry.

source
meta def tactic.mk_local' (pp_name : name) (bi : binder_info) (type : expr) :
tactic expr
source
meta def tactic.mk_local_def (pp_name : name) (type : expr) :
tactic expr
source
meta def tactic.mk_local_pis  :
expr → tactic (list expr × expr)
source
meta def tactic.get_pi_arity (type : expr) :
tactic ℕ

Compute the arity of the given (Pi-)type

source
meta def tactic.get_arity (fn : expr) :
tactic ℕ

Compute the arity of the given function

source
meta def tactic.triv  :
tactic unit
source
meta def tactic.by_contradiction (H : name) :
tactic expr
source
meta def tactic.generalizes (es : list expr) (md : tactic.transparency := semireducible) :
tactic unit
source
meta def tactic.kdependencies (e : expr) (md : tactic.transparency := reducible) :
tactic (list expr)

Return all hypotheses that depends on e The dependency test is performed using kdepends_on with the given transparency setting.

source
meta def tactic.revert_kdependencies (e : expr) (md : tactic.transparency := reducible) :
tactic ℕ

Revert all hypotheses that depend on e

source
meta def tactic.revert_kdeps (e : expr) (md : tactic.transparency := reducible) :
tactic ℕ
source
meta def tactic.cases (e : expr) (ids : list name := list.nil) (md dmd : tactic.transparency := semireducible) :
tactic (list (name × list expr))

Similar to cases_core, but e doesn't need to be a hypothesis. Remark, it reverts dependencies using revert_kdeps.

Two different transparency modes are used md and dmd. The mode md is used with cases_core and dmd with generalize and revert_kdeps.

It returns the constructor names associated with each new goal and the newly introduced hypotheses. Note that while cases_core may return "new hypotheses" that are not local constants, this tactic only returns local constants.

source
meta def tactic.refine (e : pexpr) :
tactic unit

The same as exact except you can add proof holes.

source
meta def tactic.by_cases (e : expr) (h : name) :
tactic unit

by_cases p h splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch. The expression p needs to be a proposition.

The produced proof term is dite p ?m_1 ?m_2.

source
meta def tactic.funext_core  :
list name → bool → tactic unit
source
meta def tactic.funext  :
tactic unit
source
meta def tactic.funext_lst (ids : list name) :
tactic unit
source
meta def tactic.new_aux_decl_name  :
tactic name
source
meta def tactic.abstract (tac : tactic unit) (suffix : option name := none) (zeta_reduce : bool := tt) :
tactic unit
source
meta def tactic.solve_aux {α : Type} (type : expr) (tac : tactic α) :
tactic (α × expr)

solve_aux type tac synthesize an element of 'type' using tactic 'tac'

source
meta def tactic.in_open_namespaces (d : name) :
tactic bool

Return tt iff 'd' is a declaration in one of the current open namespaces

source
meta def tactic.try_for {α : Type u_1} (max : ℕ) (tac : tactic α) :
tactic α

Execute tac for 'max' "heartbeats". The heartbeat is approx. the maximum number of memory allocations (in thousands) performed by 'tac'. This is a deterministic way of interrupting long running tactics.

source
meta def tactic.try_for_time {α : Type u_1} (max : ℕ) (tac : tactic α) :
tactic α

Execute tac for max milliseconds. Useful due to variance in the number of heartbeats taken by various tactics.

source
meta def tactic.updateex_env (f : environment → exceptional environment) :
tactic unit
source
meta def tactic.add_inductive (n : name) (ls : list name) (p : ℕ) (ty : expr) (is : list (name × expr)) (is_meta : bool := ff) :
tactic unit
source
meta def tactic.add_meta_definition (n : name) (lvls : list name) (type value : expr) :
tactic unit
source
meta def tactic.add_protected_decl (d : declaration) :
tactic unit

add declaration d as a protected declaration

source
meta def tactic.is_protected_decl (n : name) :
tactic bool

check if n is the name of a protected declaration

source
meta def tactic.add_defn_equations (lp : list name) (params : list expr) (fn : expr) (eqns : list (list pexpr × expr)) (is_meta : bool) :
tactic unit

add_defn_equations adds a definition specified by a list of equations.

The arguments:

  • lp: list of universe parameters
  • params: list of parameters (binders before the colon);
  • fn: a local constant giving the name and type of the declaration (with params in the local context);
  • eqns: a list of equations, each of which is a list of patterns (constructors applied to new local constants) and the branch expression;
  • is_meta: is the definition meta?

add_defn_equations can be used as:

 do my_add ← mk_local_def `my_add `(ℕ → ℕ),
     a ← mk_local_def `a ℕ,
     b ← mk_local_def `b ℕ,
     add_defn_equations [a] my_add
         [ ([``(nat.zero)], a),
           ([``(nat.succ %%b)], my_add b) ])
         ff -- non-meta

to create the following definition:

 def my_add (a : ℕ) : ℕ → ℕ
 | nat.zero := a
 | (nat.succ b) := my_add b
source
meta def tactic.revertible_local_context  :
tactic (list expr)

Get the revertible part of the local context. These are the hypotheses that appear after the last frozen local instance in the local context. We call them revertible because revert can revert them, unlike those hypotheses which occur before a frozen instance.

source
meta def tactic.rename_many (renames : name_map name) (strict : bool := tt) (use_unique_names : bool := ff) :
tactic unit

Rename local hypotheses according to the given name_map. The name_map contains as keys those hypotheses that should be renamed; the associated values are the new names.

This tactic can only rename hypotheses which occur after the last frozen local instance. If you need to rename earlier hypotheses, try unfreeze_local_instances.

If strict is true, we fail if name_map refers to hypotheses that do not appear in the local context or that appear before a frozen local instance. Conversely, if strict is false, some entries of name_map may be silently ignored.

If use_unique_names is true, the keys of name_map should be the unique names of hypotheses to be renamed. Otherwise, the keys should be display names.

Note that we allow shadowing, so renamed hypotheses may have the same name as other hypotheses in the context. If use_unique_names is false and there are multiple hypotheses with the same display name in the context, they are all renamed.

source
meta def tactic.rename (curr new : name) :
tactic unit

Rename a local hypothesis. This is a special case of rename_many; see there for caveats.

source
meta def tactic.rename_unstable (curr new : name) :
tactic unit

Rename a local hypothesis. Unlike rename and rename_many, this tactic does not preserve the order of hypotheses. Its implementation is simpler (and therefore probably faster) than that of rename.

source
meta def tactic.replace_hyp (h new_type eq_pr : expr) :
tactic expr

"Replace" hypothesis h : type with h : new_type where eq_pr is a proof that (type = new_type). The tactic actually creates a new hypothesis with the same user facing name, and (tries to) clear h. The clear step fails if h has forward dependencies. In this case, the old h will remain in the local context. The tactic returns the new hypothesis.

source
meta def tactic.main_goal  :
tactic expr
source
meta def tactic.with_enable_tags {α : Type} (t : tactic α) (b : bool := tt) :
tactic α
source
meta def tactic.get_main_tag  :
tactic tactic.tag
source
meta def tactic.set_main_tag (t : tactic.tag) :
tactic unit
source
meta def tactic.subst (h : expr) :
tactic unit
source
meta def list.for_each {α : Type u_1} :
list α → (α → tactic unit) → tactic unit
source
meta def list.any_of {α : Type u_1} {β : Type} :
list α → (α → tactic β) → tactic β
source
meta def order_laws_tac  :
tactic unit

Try to prove with iff.refl.

source
meta def monad_from_pure_bind {m : Type u → Type v} (pure : Π {α : Type u}, α → m α) (bind : Π {α β : Type u}, m α → (α → m β) → m β) :
monad m
source
@[protected, instance]
meta def task.monad  :
monad task
source
meta def tactic.mk_id_proof (prop pr : expr) :
expr
source
meta def tactic.mk_id_eq (lhs rhs pr : expr) :
tactic expr
source
meta def tactic.replace_target (new_target pr : expr) :
tactic unit
source
meta def tactic.eval_pexpr (α : Type) [reflected α] (e : pexpr) :
tactic α
source
meta def tactic.run_simple {α : Type u_1} :
tactic_state → tactic α → option α