namespace http://gl.mathhub.info/MMT/LFX/Finite ❚
import rules scala://FiniteTypes.LFX.mmt.kwarc.info❚
fixmeta http://cds.omdoc.org/mmt?mmt ❚
theory Symbols =
include ☞ur:?LambdaPi ❙
emptyType # ∅ ❙
emptyFun # 1 ∅f 2 prec -900 ❙
UNIT ❙
unite # ★ ❙
❚
theory TypedRules =
include ☞ur:?Typed ❙
include ☞ur:?Kinded ❙
rule rules?EmptyTypeFormation ❙
rule rules?UnitTypeFormation ❙
rule rules?UnitIntro ❙
rule rules?EmptyElim ❙
rule rules?UnitIrrelevance ❙
❚
theory SubTypedRules =
include ?TypedRules ❙
rule rules?EmptySub ❙
rule rules?EmptyFunComputation ❙
❚
theory EnumSymbols =
ENUM # ENUM 1 ❙
CASE # CASE 1 ❙
❚
theory EnumRules =
include ☞ur:?NatLiteralsOnly ❙
include ?SubTypedRules ❙
rule rules?EnumFormation ❙
rule rules?CaseIntroduction ❙
rule rules?CaseTyping ❙
rule rules?CaseSubtyping ❙
❚
theory EnumCoprodRules =
include ?EnumRules ❙
include ☞http://gl.mathhub.info/MMT/LFX/Coproducts?TypedCoproduct ❙
rule rules?EnumComputation ❙
rule rules?CaseComputation ❙
❚
theory DefinedUnitRules =
include ?TypedRules ❙
rule rules?UnitComputation ❙
rule rules?UnitElemComputation ❙
❚
theory LFFiniteBase =
include ?Symbols ❙
include ?EnumSymbols ❙
include ☞ur:?LF ❙
include ?DefinedUnitRules ❙
include ?EnumRules ❙
include ☞ur:?Ded ❙
include ☞ur:?NatRels ❙
❚
theory LFFinite =
include ?LFFiniteBase ❙
include ?EnumCoprodRules ❙
include ☞http://gl.mathhub.info/MMT/LFX/Coproducts?LFCoprod ❙
❚