package operators

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Type Members

  1. abstract class DiagramOperator extends ComputationRule
  2. abstract class FunctorialLinearDiagramOperator[HelperContextType <: LinearTheoryOperatorContext] extends DiagramOperator with MorphismOperatorFromLinearTheoryOperatorMixin[HelperContextType]
  3. trait LinearTheoryOperator[HelperContextType <: LinearTheoryOperatorContext] extends SublinearTheoryOperator[HelperContextType]
  4. class LinearTheoryOperatorContext extends UnaryTheoryOperatorContext
  5. trait MorphismOperatorFromLinearTheoryOperatorMixin[HelperContextType <: LinearTheoryOperatorContext] extends UnaryMorphismOperator[HelperContextType] with LinearTheoryOperator[HelperContextType]
  6. case class NotApplicable[T]() extends OperatorResult[T] with Product with Serializable
  7. sealed abstract class OperatorResult[T] extends AnyRef
  8. trait Pushout extends ConstantScala

    apply/unapply methods for terms of the form Combine(diagram1, List(Rename1(old1,new1),...), diagram2, List(Rename1(old2,new2),...))

  9. trait SublinearTheoryOperator[HelperContextType <: UnaryTheoryOperatorContext] extends UnaryTheoryOperator
  10. case class TransformedResult[T](result: T) extends OperatorResult[T] with Product with Serializable
  11. trait UnaryMorphismOperator[HelperContextType <: UnaryTheoryOperatorContext] extends AnyRef
  12. trait UnaryTheoryOperator extends AnyRef
  13. class UnaryTheoryOperatorContext extends AnyRef

Value Members

  1. object Combinators
  2. object Combine extends Pushout
  3. object Common
  4. object ComputeCombine extends ComputationRule
  5. object ComputeDiagramAccess extends ComputationRule
  6. object ComputeEmpty extends ComputationRule

    Empty(p) ---> p{}

  7. object ComputeExpand extends ComputationRule
  8. object ComputeExtends extends ComputationRule
  9. object ComputeHom extends ComputationRule
  10. object ComputeMixin extends ComputationRule

    Translate(m,T) and Expand(m,T) form a pushout along an inclusion as follows:

    Translate(m,T) and Expand(m,T) form a pushout along an inclusion as follows:

    m : A -> B inclusion from A to T Expand(m,T): T -> Translate(m,T) inclusion from B to Translate(m,T)

  11. object ComputePushoutAlongInclusion extends ComputationRule
  12. object ComputeRename extends ComputationRule
  13. object DiagramAccessor extends BinaryConstantScala
  14. object Empty extends UnaryConstantScala

    operator for the empty theory of a given meta-theory

  15. object Expand extends BinaryConstantScala

    see Mixin

  16. object Extends extends FlexaryConstantScala
  17. object Hom extends UnaryConstantScala
  18. object Mixin extends Pushout
  19. object NamedPushoutUtils
  20. object NewPushoutUtils

    Helper functions for computing pushouts of anonymous theories.

    Helper functions for computing pushouts of anonymous theories.

    To do

    Rename to sensible name, beware that PushoutUtils is already taken by Common.scala in the same directory.

  21. object PL extends TheoryScala

    MMT declarations

    MMT declarations

    namespace http://cds.omdoc.org/examples fixmeta ?LF

    theory PL = prop : type ded : prop -> type

    theory SFOL = sort : type term : sort -> type

  22. object PushoutAlongInclusion extends BinaryConstantScala
  23. object PushoutUtils
  24. object Rename extends FlexaryConstantScala
  25. object Rename1 extends BinaryConstantScala
  26. object SFOL extends TheoryScala

    The SFOL theory from the MMT/examples archive

  27. object TypedTerms extends TheoryScala

Ungrouped