gapt.proofs.context.facet

Base types, including inductive types.

Constant symbols, including defined constants, constructors, etc.

Definitions that define a constant by an expression of the same type.

Type class for a facet of a context.

A facet collects some kind of information that is relevant to a context. A facet may for example collect all the base types (uninterpreted, struturally inductive, etc.) currently declared in a context.

Definitional reductions.

Inductive types, for each type we store its list of constructors.