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

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

theory Symbols =
	Coprod # 1⨁…  prec -10000❙
	inl # 1 ↪l 2 prec -5 ❙
	inr # 2 r↩ 1 prec -5 ❙
	coprodmatch # 2 match V1 . 3|… to 4 %I5 prec -9000❙
	coprodmatch2 # 2 match 5 , V1 . 3|… to 4 prec -9001❙
❚
	
theory FuncaddSymbol =
	Addfunc # 1⊕… prec 0❙
❚
	
theory SimpleRules =
   rule rules?CoprodTerm ❙
   rule rules?inlTerm ❙
   rule rules?inrTerm ❙
   rule rules?MatchTerm ❙
   rule rules?MatchComp ❙
   // rule rules?MatchEquality ❙
   rule rules?CoprodSubType ❙
❚

theory TypedCoproduct : ur:?TermsTypesKinds =
	include ?Symbols ❙
  include ?SimpleRules ❙
❚


theory FuncaddRules =
	rule rules?AddFuncComp ❙
❚

theory LFCoprod =
	include ?FuncaddSymbol ❙
	include ?FuncaddRules ❙
	include ?TypedCoproduct ❙
	include ☞ur:?LF ❙
❚