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.

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

def tactic_doc.attribute.ancestor :

tactic_doc_entry

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.