mathlib documentation

tactic.algebra

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

On failure, the empty list is returned.

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

On failure, the empty list is returned.

meta def tactic.find_ancestors  :

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

On failure, the empty list is returned.