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❙
❚