p

info.kwarc.mmt.lf

structuralfeatures

package structuralfeatures

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Type Members

  1. class Constructor extends TermLevel
  2. class InductiveDefinitions extends StructuralFeature with TypedParametricTheoryLike

    theories as a set of types of expressions

  3. class InductiveMatch extends StructuralFeature with TypedParametricTheoryLike

    theories as a set of types of expressions

  4. class InductiveProofDefinitions extends StructuralFeature with TypedParametricTheoryLike

    theories as a set of types of expressions

  5. class InductiveTypes extends StructuralFeature with ParametricTheoryLike

    theories as a set of types of expressions

  6. sealed abstract class InternalDeclaration extends AnyRef

    helper class for the various declarations in an inductive type

  7. class OutgoingTermLevel extends TermLevel
  8. class RecordDefinitions extends StructuralFeature with TypedParametricTheoryLike

    theories as a set of types of expressions

  9. class Records extends StructuralFeature with ParametricTheoryLike

    theories as a set of types of expressions

  10. class Reflections extends StructuralFeature with TypedParametricTheoryLike

    theories as a set of types of expressions

  11. case class StatementLevel(path: GlobalName, args: List[(Option[LocalName], Term)], df: Option[Term] = None, ctx: Option[Context] = None, notC: Option[NotationContainer] = None) extends InternalDeclaration with Product with Serializable

    Rules and Judgment constructors

  12. abstract case class TermLevel(path: GlobalName, args: List[(Option[LocalName], Term)], ret: Term, df: Option[Term] = None, notC: Option[NotationContainer] = None, ctx: Option[Context] = None) extends InternalDeclaration with Product with Serializable

    term constructor declaration

  13. case class TypeLevel(path: GlobalName, args: List[(Option[LocalName], Term)], df: Option[Term], ctx: Option[Context] = None, notC: Option[NotationContainer] = None) extends InternalDeclaration with Product with Serializable

    type declaration

  14. class EquivalenceRelation extends StructuralFeature with ParametricTheoryLike
    Annotations
    @MMT_TODO( message = ... )
    Deprecated

    this is experimental and may still be removed

  15. class Quotients extends StructuralFeature with ParametricTheoryLike
    Annotations
    @MMT_TODO( message = ... )
    Deprecated

    this is experimental and may still be removed

  16. class Subtypes extends StructuralFeature with ParametricTheoryLike
    Annotations
    @MMT_TODO( message = ... )
    Deprecated

    this is experimental and may still be removed

Value Members

  1. object Constructor extends Serializable
  2. object EquivalenceRelationRule extends StructuralFeatureRule
  3. object InductiveDefinitionRule extends StructuralFeatureRule
  4. object InductiveMatchRule extends StructuralFeatureRule
  5. object InductiveProofDefinitionRule extends StructuralFeatureRule
  6. object InductiveRule extends StructuralFeatureRule
  7. object InductiveTypes
  8. object InternalDeclaration
  9. object OutgoingTermLevel extends Serializable
  10. object QuotientRule extends StructuralFeatureRule
  11. object RecordDefinitionRule extends StructuralFeatureRule
  12. object RecordRule extends StructuralFeatureRule
  13. object RecordUtil
  14. object ReflectionRule extends StructuralFeatureRule
  15. object StatementLevel extends Serializable
  16. object StructuralFeatureUtils
  17. object SubtypeRule extends StructuralFeatureRule
  18. object TermConstructingFeatureUtil
  19. object TypeLevel extends Serializable
  20. object inductiveUtil

Ungrouped