package moduleexpressions
- Alphabetic
- Public
- All
Type Members
-
class
ElaboratedConstant extends LazyConstant
produced and added by InstanceElaborator
-
class
InstanceElaborator extends ChangeListener
elaborates each instance that is added
elaborates each instance that is added
instances are constant whose type is THEORY
Value Members
- object AnonymousTheoryInfer extends InferenceRule
-
object
ComplexTheoryInfer extends InferenceRule
C Context ---> {{C}} : theory
-
object
CompositionInfer extends InferenceRule
m1: a1 => b1 and m2: a2 => b2 and b1 <= a2 ---> m1;m2: a1 => b2
m1: a1 => b1 and m2: a2 => b2 and b1 <= a2 ---> m1;m2: a1 => b2
cannot infer type of empty composition
-
object
IdentityInfer extends InferenceRule
T: theory ---> id_T : T=>T
-
object
MorphCheck extends TypingRule
m : MOR A B
-
object
MorphTypeInhabitable extends InhabitableRule
MOR A B : Inhabitable
-
object
MorphismApplicationCompute extends ComputationRule
apply a morphism
apply a morphism
t APPLY m ----> m(t)
-
object
MorphismApplicationTerm extends InferenceRule
typing is preserved along morphisms
typing is preserved along morphisms
m: MOR mDom mCod and mDom |- t : a ---> mCod |- t APPLY m : a APPLY m
-
object
TheoryTypeInhabitable extends InhabitableRule
THY : Inhabitable
-
object
TheoryTypeUniverse extends UniverseRule
THY : Universe