namespace http://gl.mathhub.info/MMT/LFX/IntersectionTypes ❚
import rules scala://LFIntersectionTypes.LFX.mmt.kwarc.info ❚
import lfrules scala://lf.mmt.kwarc.info❚
fixmeta http://cds.omdoc.org/mmt?mmt ❚
theory Symbols =
typeintersection # 1⊓… prec -9999 ❙
❚
theory Rules =
include ☞ur:?TermsTypesKinds ❙
rule rules?IntersectionTypeRule ❙
rule rules?IntersectionTyping ❙
rule rules?IntersectionSubtypeRuleLeft ❙
rule rules?IntersectionSubtypeRuleRight ❙
❚
theory LFIntersectionTypes =
include ☞ur:?LambdaPi ❙
include ?Symbols ❙
include ?Rules ❙
rule lfrules?PiType❙
rule lfrules?PiTerm❙
// rule lfrules?ApplyTerm❙
rule lfrules?LambdaTerm❙
rule lfrules?Beta❙
rule lfrules?Extensionality❙
rule lfrules?PiCongruence❙
rule lfrules?LambdaCongruence❙
rule lfrules?Solve❙
rule lfrules?SolveType❙
rule lfrules?TheoryTypeWithLF❙
rule lfrules?PiIntroduction❙
rule lfrules?ForwardPiElimination❙
rule lfrules?BackwardPiElimination❙
rule lfrules?LFHOAS❙
rule rules?ApplyIntersection ❙
❚