mathlib3 documentation

tactic.algebra

Recording typeclass ancestors #

The "old" structure command currently does not record the parent typeclasses. This file defines the ancestor attribute to remedy this. This information is notably used by to_additive to map structure fields and constructors of a multiplicative structure to its additive counterpart.

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.

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.

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

On failure, the empty list is returned.

meta def tactic.get_ancestors (cl : name) :

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

On failure, the empty list is returned.

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

On failure, the empty list is returned.