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.

inductive tactic.decl_reducibility  :
Type

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

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

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} :

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