namespace http://cds.omdoc.org/urtheories❚
import meta http://cds.omdoc.org/mmt❚
import rules scala://lf.mmt.kwarc.info❚
rule scala://parser.api.mmt.kwarc.info?MMTURILexer❚
theory Typed =
type❙
equality # equality 1 2 ❘ role Eq❙
oftype # 1 : 2 prec -9997 ❘ role Type❙
definedas # 1 := 2 prec -9998 ❘ role Def❙
withnotation # 1 # 2 prec -9998 ❘ role Notation❙
❚
theory Kinded =
include ?Typed❙
kind❙
❚
theory TypedConstants =
rule rules?UniverseType❙
rule rules?TypeInhabitable❙
❚
theory KindedConstants =
rule rules?UniverseKind❙
rule rules?KindInhabitable❙
❚
theory TermsTypesKinds =
include ☞meta:?Errors❙
include ?ModExp❙
include ☞meta:?mmt❙
include ?Typed❙
include ?Kinded❙
include ?TypedConstants❙
include ?KindedConstants❙
rule rules?UnivTerm❙
rule rules?TypeAttributionTerm❙
rule rules?DropTypeAttribution❙
❚
theory LambdaPi =
include ?Kinded❙
Pi # { V1T,… } 2 prec -10000❙
lambda # [ V1T,… ] 2 prec -10000❙
apply # 1%w… prec -10❙
arrow # 1⟶… prec -9990❙
❚
theory LFRules =
include ?LambdaPi❙
rule rules?PiType❙
rule rules?PiTerm❙
rule rules?ApplyTerm❙
rule rules?LambdaTerm❙
rule rules?Beta❙
rule rules?Extensionality❙
rule rules?PiCongruence❙
rule rules?LambdaCongruence❙
// rule rules?NormalizeCurrying❙
rule rules?FlattenCurrying❙
rule rules?Solve❙
rule rules?SolveType❙
rule rules?TheoryTypeWithLF❙
rule rules?PiIntroduction❙
rule rules?ForwardPiElimination❙
rule rules?BackwardPiElimination❙
rule rules?PiIrrelevanceRule❙
rule rules?LFHOAS❙
❚
theory LF =
include ?TermsTypesKinds❙
include ?LambdaPi❙
include ?LFRules❙
❚
theory ShallowPolymorphism =
include ?Typed❙
rule rules?ShallowPolymorphism❙
rule rules?PolymorphicApplyTerm❙
❚
theory PLF =
include ?LF❙
include ?ShallowPolymorphism❙
❚