package operators
- Alphabetic
- Public
- All
Type Members
- abstract class DiagramOperator extends ComputationRule
- abstract class FunctorialLinearDiagramOperator[HelperContextType <: LinearTheoryOperatorContext] extends DiagramOperator with MorphismOperatorFromLinearTheoryOperatorMixin[HelperContextType]
- trait LinearTheoryOperator[HelperContextType <: LinearTheoryOperatorContext] extends SublinearTheoryOperator[HelperContextType]
- class LinearTheoryOperatorContext extends UnaryTheoryOperatorContext
- trait MorphismOperatorFromLinearTheoryOperatorMixin[HelperContextType <: LinearTheoryOperatorContext] extends UnaryMorphismOperator[HelperContextType] with LinearTheoryOperator[HelperContextType]
- case class NotApplicable[T]() extends OperatorResult[T] with Product with Serializable
- sealed abstract class OperatorResult[T] extends AnyRef
-
trait
Pushout extends ConstantScala
apply/unapply methods for terms of the form Combine(diagram1, List(Rename1(old1,new1),...), diagram2, List(Rename1(old2,new2),...))
- trait SublinearTheoryOperator[HelperContextType <: UnaryTheoryOperatorContext] extends UnaryTheoryOperator
- case class TransformedResult[T](result: T) extends OperatorResult[T] with Product with Serializable
- trait UnaryMorphismOperator[HelperContextType <: UnaryTheoryOperatorContext] extends AnyRef
- trait UnaryTheoryOperator extends AnyRef
- class UnaryTheoryOperatorContext extends AnyRef
Value Members
- object Combinators
- object Combine extends Pushout
- object Common
- object ComputeCombine extends ComputationRule
- object ComputeDiagramAccess extends ComputationRule
-
object
ComputeEmpty extends ComputationRule
Empty(p) ---> p{}
- object ComputeExpand extends ComputationRule
- object ComputeExtends extends ComputationRule
- object ComputeHom extends ComputationRule
-
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)
- object ComputePushoutAlongInclusion extends ComputationRule
- object ComputeRename extends ComputationRule
- object DiagramAccessor extends BinaryConstantScala
-
object
Empty extends UnaryConstantScala
operator for the empty theory of a given meta-theory
-
object
Expand extends BinaryConstantScala
see Mixin
- object Extends extends FlexaryConstantScala
- object Hom extends UnaryConstantScala
- object Mixin extends Pushout
- object NamedPushoutUtils
-
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.
-
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
- object PushoutAlongInclusion extends BinaryConstantScala
- object PushoutUtils
- object Rename extends FlexaryConstantScala
- object Rename1 extends BinaryConstantScala
-
object
SFOL extends TheoryScala
The SFOL theory from the
MMT/examples
archive - object TypedTerms extends TheoryScala