namespace http://gl.mathhub.info/MMT/LFX/Datatypes ❚
import rules scala://datatypes.LFX.mmt.kwarc.info❚

fixmeta http://cds.omdoc.org/mmt?mmt ❚

theory ListSymbols =
   ListType # List 1 prec -500 ❙
   nil ❙
   ls # ls 1,… prec -500❙
   append # 1 ++ 2 ❙
   map # 1 map 2 ❙
❚

theory ListRules =
	rule rules?ListTypeRule ❙
	rule rules?ListVariance ❙
	rule rules?ListCheckRule ❙
	rule rules?AppendType ❙
	rule rules?MapType ❙
	rule rules?MapComp ❙
❚

theory LFLists =
	include ?ListSymbols ❙
	include ?ListRules ❙
	include ☞ur:?LF ❙
❚

theory LetSymbol =
    Let # Let V1 = 2 in 3 prec -5000 ❙
❚

theory LetRules =
    rule rules?LetRule ❙
❚

theory LFLet =
    include ?LetSymbol ❙
    include ?LetRules ❙
    include ☞ur:?LF ❙
❚

theory SubSymbol =
    substitute # 1 sub 2 / 3 prec -5000 ❙
❚

theory SubRules =
    rule rules?SubRule ❙
❚

theory LFSub =
    include ?SubSymbol ❙
    include ?SubRules ❙
    include ☞ur:?LF ❙
❚