package reflection
- Alphabetic
- Public
- All
Value Members
-
object
Computation extends ComputationRule
|- m: p -> .
|- m: p -> . ---> |- elim(refl(p, t), m) = m(t)
-
object
ElimInfer extends InferenceRule
|- t: formation(p,a) ---> |- elim(t,m) : m(a)
-
object
Extensionality extends ExtensionalityRule
p |- eval(t1) = eval(t2): a ---> |- t1 = t2 : formation(p,a)
-
object
FormationInfer extends InferenceRule
p |- t: U ---> |- formation(p,t) : U
-
object
ReflInfer extends InferenceRule
p |- t: a ---> |- refl(p,t) : formation(p,a)
- object Terms extends TheoryScala
-
object
TypingRule extends api.checking.TypingRule
p |- eval(t) : a ---> |- q: formation(p,a)