namespace http://gl.mathhub.info/MMT/LFX/Records 
import rules scala://Records.LFX.mmt.kwarc.info
import rules2 scala://LFX.mmt.kwarc.info 

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

theory Symbols =
	include ☞http://cds.omdoc.org/urtheories?ModExp 
	
  Rectype # {' L1Td, '} prec -10000 
  Recexp  # [' L1Dd, '] prec -12000 
  Getfield # 1 . L2 prec 100000 
  ModelsOf # Mod 1 prec -1000 
  // ModelsOfUnary # Mod 1 prec -999 ❙
  // AsInstance # AsInstance 1 prec -1000 ❙
  RecordMerge # 1 prec 0


  
theory Rules =
  rule rules?GetFieldComp 
  // rule rules?GetFieldInType ❙
  rule rules?GetfieldTerm 
  rule rules?RecEquality 
  rule rules?RecExpCongruence 
  rule rules?RecordExpTerm 
  rule rules?RecordTypeTerm 
  rule rules?RecSubtype 
  rule rules?RecTypeCheck 
  rule rules?RecTypeCongruence 
  rule rules?CanonicalSolution
  // rule rules?ModelsRule ❙
  rule rules?ModelsInference 
  rule rules?ModelsChecking 
  rule rules?Instance 
  rule rules?ExtendInstance 
  rule rules?RecordMergeInference 
  rule rules?MergeCheck 


theory TypedRecords =
	include ☞ur:?TermsTypesKinds 
	include ?Symbols 
	include ?Rules 

  
theory LFRecords =
	include ☞ur:?LF 
	include ?TypedRecords