mathlib documentation

tactic.algebra

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 (a : name) (a_1 : 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.