mathlib documentation

tactic.with_local_reducibility

with_local_reducibility #

Run a tactic in an environment with a temporarily modified reducibility attribute for a specified declaration.

source
inductive tactic.decl_reducibility  :
Type

Possible reducibility attributes for a declaration: reducible, semireducible (the default), irreducible.

source
@[protected, instance]
def tactic.decl_reducibility.decidable_eq  :
decidable_eq tactic.decl_reducibility
source
@[protected, instance]
def tactic.decl_reducibility.inhabited  :
inhabited tactic.decl_reducibility

Satisfy the inhabited linter

Equations
source
meta def tactic.get_decl_reducibility (n : name) :
tactic tactic.decl_reducibility

Get the reducibility attribute of a declaration. Fails if the name does not refer to an existing declaration.

source
def tactic.decl_reducibility.to_attribute  :
tactic.decl_reducibility → name

Return the attribute (as a name) corresponding to a reducibility level.

Equations
source
meta def tactic.set_decl_reducibility (n : name) (r : tactic.decl_reducibility) (persistent : bool := ff) :
tactic unit

Set the reducibility attribute of a declaration. If persistent := ff, this is scoped to the enclosing section, like local attribute.

source
meta def tactic.with_local_reducibility {α : Type} (n : name) (r : tactic.decl_reducibility) (body : tactic α) :
tactic α

Execute a tactic with a temporarily modified reducibility attribute for a declaration.