mathlib documentation

tactic.algebra

source
meta def tactic.ancestor_attr  :
user_attribute unit (list name)

The ancestor attributes is used to record the names of structures which appear in the extends clause of a structure or class declared with old_structure_cmd set to true.

As an example:

set_option old_structure_cmd true

structure base_one := (one : ℕ)

structure base_two (α : Type*) := (two : ℕ)

@[ancestor base_one base_two]
structure bar extends base_one, base_two α

The list of ancestors should be in the order they appear in the extends clause, and should contain only the names of the ancestor structures, without any arguments.

source
meta def tactic.get_tagged_ancestors (cl : name) :
tactic (list name)

Returns the parents of a structure added via the ancestor attribute.

On failure, the empty list is returned.

source
meta def tactic.get_ancestors (cl : name) :
tactic (list name)

Returns the parents of a structure added via the ancestor attribute, as well as subobjects.

On failure, the empty list is returned.

source
meta def tactic.find_ancestors  :
name → expr → tactic (list expr)

Returns the (transitive) ancestors of a structure added via the ancestor attribute (or reachable via subobjects).

On failure, the empty list is returned.