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

reducible : tactic.decl_reducibility
semireducible : tactic.decl_reducibility
irreducible : tactic.decl_reducibility

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

@[instance]

def tactic.decl_reducibility.decidable_eq :

decidable_eq tactic.decl_reducibility

@[instance]

def tactic.inhabited :

inhabited tactic.decl_reducibility

Satisfy the inhabited linter

Equations

tactic.inhabited = {default := tactic.decl_reducibility.semireducible}

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.

def tactic.decl_reducibility.to_attribute (a : tactic.decl_reducibility) :

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

Equations

tactic.decl_reducibility.irreducible.to_attribute = name.mk_string "irreducible" name.anonymous
tactic.decl_reducibility.semireducible.to_attribute = name.mk_string "semireducible" name.anonymous
tactic.decl_reducibility.reducible.to_attribute = name.mk_string "reducible" name.anonymous

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

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} (n : name) (r : tactic.decl_reducibility) (body : tactic α) :

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