with_local_reducibility
Run a tactic in an environment with a temporarily modified reducibility attribute for a specified declaration.
- reducible : tactic.decl_reducibility
- semireducible : tactic.decl_reducibility
- irreducible : tactic.decl_reducibility
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.
def
tactic.with_local_reducibility
{α : Type} :
name → tactic.decl_reducibility → tactic α → tactic α
Execute a tactic with a temporarily modified reducibility attribute for a declaration.