# mathlibdocumentation

tactic.with_local_reducibility

# with_local_reducibility

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

inductive tactic.decl_reducibility  :
Type

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

@[instance]

@[instance]

Satisfy the inhabited linter

Equations

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

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

Equations

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

meta def tactic.with_local_reducibility {α : Type} :
name

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