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

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

theory Symbols =
	wtype # W V1T . 2 prec -10000 ❙
	sup # sup 2 , V1 ⟹ 3 to 4 prec -8000 ❙
	rec # rec 4 , V1 , V2 , V3 ⟹ 5 to 6  prec -8000 ❙
❚
	
theory Rules =   
   rule rules?WTypeFormation ❙
   rule rules?SupIntroduction ❙
   rule rules?WEquality ❙
   rule rules?RecElimination ❙
   rule rules?RecComputation ❙
   // rule info.kwarc.mmt.LFX.WTypes.supEquality ❙
❚
   

theory WTypes =
	include ☞ur:?LF ❙
	include ?Symbols ❙
	include ?Rules ❙
❚
	
theory LFW =
	include ?WTypes ❙
	include ☞http://gl.mathhub.info/MMT/LFX/Finite?LFFinite ❙
❚

theory Inductive =
	include ?LFW ❙
	include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
	rule rules?InductiveTypes ❙
	rule rules?InductiveDefs ❙
❚