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 ❙
❚