Base
structure PhysicalConstants
domain?PhysicalConstants
structure LFSigma
domain?LFSigma
structure TypedSigma
domain?TypedSigma
structure Symbols
domain?Symbols
structure Rules
domain?Rules
structure LF
domain?LF
structure TermsTypesKinds
domain?TermsTypesKinds
structure Errors
domain?Errors
structure ModExp
domain?ModExp
structure mmt
domain?mmt
structure Typed
domain?Typed
structure Kinded
domain?Kinded
structure TypedConstants
domain?TypedConstants
structure KindedConstants
domain?KindedConstants
structure LambdaPi
domain?LambdaPi
structure LFRules
domain?LFRules
constant exp
type
constant der
type{P:bool}(((predP))((predP)))
parsing-notationb ' (precedence 0)
constant Real_vec_space2
typetype
definition×
parsing-notationℝ2 (precedence 0)
constant Real_vec_space3
typetype
definition××
parsing-notationℝ3 (precedence 0)
constant comp1
typeℝ3
definition[v:ℝ3](πlv)
constant comp2
typeℝ3
definition[v:ℝ3](πl(πrv))
constant comp3
typeℝ3
definition[v:ℝ3](πr(πrv))
constant pred_as_sub2
type(ℝ2bool)type
definition[P:ℝ2bool]ℝ2|([z:ℝ2]((Pz)))
parsing-notationpred2 a (precedence 0)
constant pred_as_sub3
type(ℝ3bool)type
definition[P:ℝ3bool]ℝ3|([z:ℝ3]((Pz)))
parsing-notationpred3 a (precedence 0)
constant lift_type_one_to_three
type(bool)(ℝ3bool)
definition[P:bool]([v:ℝ3](((P(comp1v))((comp2v)0))((comp3v)0)))
parsing-notationt1↑ a (precedence 0)
constant lift_type_two_to_three
type(ℝ2bool)(ℝ3bool)
definition[P:ℝ2bool]([v:ℝ3]((P(comp1v),(comp2v))((comp3v)0)))
parsing-notationt2↑ a (precedence -1)
constant lift_function_one_to_three
type{P:bool}(((predP))((pred3(t1↑P))))
parsing-notationf1↑ b (precedence 0)
constant lift_function_two_to_three
type{P:ℝ2bool}(((pred2P))((pred3(t2↑P))))
parsing-notationf2↑ b (precedence 0)