Type Members

1.  case class ArbitraryScript(opener: String, scrpt: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
2.  case class ArgAlgebraicOrderSimplifier(specs: List[ArgAlgebraicOrderSimplifierSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
3.  case class ArgAlgebraicOrderSimplifierSpec(names: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
4.  case class ArgAlgebraicProcessor(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
5.  case class ArgAlgebraicSimplifier(specs: List[ArgAlgebraicSimplifierSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
6.  case class ArgAlgebraicSimplifierSpec(names: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
7.  case class ArgAlgebraicTermComparator(specs: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
8.  case class ArgApplicabilityRecognizer(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
9.  case class ArgAssumptions(defs: List[DefString], frms: List[IMPSMathExp], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
10.  case class ArgAxioms(cps: List[AxiomSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
11.  case class ArgBase(sf: ArgSpecForms, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
12.  case class ArgBaseCaseHook(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
13.  case class ArgBaseTheory(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
14.  case class ArgBaseTypes(nms: List[IMPSSort], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
15.  case class ArgBinding(n: Int, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
16.  case class ArgCoefficient(sf: ArgSpecForms, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
17.  case class ArgComponentSections(nms: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
18.  case class ArgComponentTheories(cps: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
19.  case class ArgConstAssoc(nm: Name, consts: List[ODefString], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
20.  case class ArgConstPairSpec(name: Name, const: ODefString, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
21.  case class ArgConstPairs(defs: List[ArgConstPairSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
22.  case class ArgConstantSpec(nm: Name, enc: IMPSSort, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
23.  case class ArgConstants(specs: List[ArgConstantSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
24.  case class ArgCoreTranslation(tr: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
25.  case class ArgDefStringList(dfs: List[DefString], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
26.  case class ArgDefinitionName(dn: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
27.  case class ArgDiscreteSorts(srts: List[IMPSSort], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
28.  case class ArgDistinctConstants(ds: List[List[Name]], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
29.  case class ArgDontUnfold(nms: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
30.  case class ArgEmbeddedLang(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
31.  case class ArgEmbeddedLangs(nms: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
32.  case class ArgEnsembleConsts(consts: List[ArgConstAssoc], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
33.  case class ArgEnsembleSorts(sorts: List[ArgSortAssoc], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
34.  case class ArgExponent(sf: ArgSpecForms, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
35.  case class ArgExtensible(specs: List[ArgTypeSortAList], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
36.  case class ArgFileSpec(nm1: Name, nm2: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
37.  case class ArgFiles(nms: List[ArgFileSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
38.  case class ArgFixedTheories(ts: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
39.  case class ArgHomeTheory(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
40.  case class ArgInductionPrinciple(p: Either[Name, DefString], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
41.  case class ArgInductionStepHook(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
42.  case class ArgLanguage(lang: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
43.  case class ArgLeftMethod(mn: ParseMethod.ParseMethod, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
44.  case class ArgMacete(mn: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
45.  case class ArgMethod(mn: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
46.  case class ArgMultiples(ns: List[Number], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
47.  case class ArgNameList(nms: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
48.  case class ArgNewTranslationName(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
49.  case class ArgNullMethod(mn: ParseMethod.ParseMethod, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
50.  case class ArgNumbers(ns: List[Number], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
51.  case class ArgOperationAlist(optype: OperationType.OperationType, op: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
52.  case class ArgOperations(defs: List[ArgOperationAlist], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
53.  case class ArgOperationsAlist(optype: Name, op: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
54.  case class ArgOverloadingPair(tname: Name, sname: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
55.  case class ArgPairs(ps: List[ArgRenamerPair], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
56.  case class ArgPermutations(nns: List[List[Number]], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
57.  case class ArgProcOperations(alists: List[ArgOperationsAlist], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
58.  case class ArgProof(prf: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
59.  case class ArgRenamer(rn: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
60.  case class ArgRenamerPair(old: Name, nu: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
61.  case class ArgReplicaRenamer(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
62.  case class ArgRetrievalProtocol(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
63.  case class ArgScalars(ntype: NumericalType.NumericalType, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
64.  case class ArgSet(cont: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
65.  case class ArgSort(srt: IMPSSort, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
66.  case class ArgSortAssoc(nm: Name, sorts: List[ODefString], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
67.  case class ArgSortPairSpec(name: Name, srt: Either[Either[Name, DefString], Either[DefString, DefString]], mth: Option[IMPSMathExp], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
68.  case class ArgSortPairs(defs: List[ArgSortPairSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
69.  case class ArgSortSpec(sub: IMPSSort, enc: IMPSSort, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
70.  case class ArgSorts(specs: List[ArgSortSpec], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
71.  case class ArgSource(thy: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
72.  case class ArgSourceTheories(nms: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
73.  case class ArgSourceTheory(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
74.  case class ArgSpecForms(specform: Either[Name, QDFSpecForm], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
75.  case class ArgSpecialRenamings(ns: List[ArgRenamerPair], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
76.  case class ArgTable(tn: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
77.  case class ArgTarget(thy: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
78.  case class ArgTargetMultiple(n: Number, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
79.  case class ArgTargetTheories(ns: List[Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
80.  case class ArgTheory(thy: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
81.  case class ArgTheoryInterpretationCheck(cm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
82.  case class ArgToken(t: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
83.  case class ArgTranslation(t: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
84.  case class ArgTypeSortAList(tp: NumericalType.NumericalType, srt: IMPSSort, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
85.  case class ArgUsages(usgs: List[Usage.Usage], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
86.  case class ArgWitness(w: DefString, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
87.  case class AxiomSpec(name: Option[String], defstr: DefString, frm: Option[IMPSMathExp], usgs: Option[List[Usage.Usage]], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
88.  type CommentInfo = Option[LineComment]
89.  abstract class Comp[T <: DefForm] extends Logger
90.  case class DFAlgebraicProcessor(nm: Name, canc: Option[ModCancellative], lang: ArgLanguage, bs: ArgBase, ex: Option[ArgExponent], co: Option[ArgCoefficient], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
91.  case class DFAtomicSort(name: Name, dfs: DefString, frm: IMPSMathExp, sort: IMPSSort, thy: ArgTheory, usgs: Option[ArgUsages], wtn: Option[ArgWitness], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
92.  class DFAtomicSortC extends Comp[DFAtomicSort]
93.  case class DFComment(c: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
94.  case class DFCompoundMacete(nm: Name, spec: MaceteSpec, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
95.  case class DFConstant(name: Name, dfs: DefString, frm: IMPSMathExp, sort: IMPSSort, thy: ArgTheory, srt: Option[ArgSort], usgs: Option[ArgUsages], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
96.  class DFConstantC extends Comp[DFConstant]
97.  case class DFImportedRewriteRules(nm: Name, thy: Option[ArgSourceTheory], thies: Option[ArgSourceTheories], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
98.  case class DFIncludeFiles(rl: Option[ModReload], ql: Option[ModQuickLoad], fs: Option[ArgFiles], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
99.  case class DFInductor(nm: Name, princ: ArgInductionPrinciple, thy: ArgTheory, trans: Option[ArgTranslation], bh: Option[ArgBaseCaseHook], ih: Option[ArgInductionStepHook], du: Option[ArgDontUnfold], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
100.  case class DFLanguage(name: Name, els: Option[ArgEmbeddedLangs], el: Option[ArgEmbeddedLang], bt: Option[ArgBaseTypes], srts: Option[ArgSorts], ex: Option[ArgExtensible], cnsts: Option[ArgConstants], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
101.  case class DFLoadSection(sc: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
102.  case class DFOrderProcessor(nm: Name, ap: Option[ArgAlgebraicProcessor], ops: Option[ArgProcOperations], ds: Option[ArgDiscreteSorts], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
103.  case class DFOverloading(n: Name, ps: List[ArgOverloadingPair], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
104.  case class DFParseSyntax(n: Name, t: Option[ArgToken], lm: Option[ArgLeftMethod], nm: Option[ArgNullMethod], tbl: Option[ArgTable], bnd: ArgBinding, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
105.  case class DFPrintSyntax(n: Name, tex: Option[ModTex], t: Option[ArgToken], m: Option[ArgMethod], tbl: Option[ArgTable], bnd: ArgBinding, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
106.  case class DFQuasiConstructor(name: Name, dfs: DefString, lan: ArgLanguage, fx: Option[ArgFixedTheories], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
107.  case class DFRecursiveConstant(ns: ArgNameList, defs: ArgDefStringList, frms: List[IMPSMathExp], srts: List[IMPSSort], thy: ArgTheory, usgs: Option[ArgUsages], defname: Option[ArgDefinitionName], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
108.  class DFRecursiveConstantC extends Comp[DFRecursiveConstant]
109.  case class DFRenamer(nm: Name, ps: Option[ArgPairs], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
110.  case class DFSchematicMacete(name: Name, dfs: DefString, nil: Option[ModNull], trans: Option[ModTransportable], t: ArgTheory, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
111.  case class DFScript(nm: Name, argc: Number, scrpt: Script, ret: Option[ArgRetrievalProtocol], rec: Option[ArgApplicabilityRecognizer], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
112.  case class DFSection(nm: Name, com: Option[ArgComponentSections], fls: Option[ArgFiles], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
113.  case class DFTheorem(n: Name, defn: ODefString, frm: Option[IMPSMathExp], modr: Option[ModReverse], modl: Option[ModLemma], t: ArgTheory, us: Option[ArgUsages], tr: Option[ArgTranslation], mac: Option[ArgMacete], ht: Option[ArgHomeTheory], prf: Option[ArgProof], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
114.  class DFTheoremC extends Comp[DFTheorem]
115.  case class DFTheory(name: Name, lang: Option[ArgLanguage], comp: Option[ArgComponentTheories], axioms: Option[ArgAxioms], dstnct: Option[ArgDistinctConstants], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
116.  class DFTheoryC extends Comp[DFTheory]
117.  case class DFTheoryEnsemble(nm: Name, bt: Option[ArgBaseTheory], fts: Option[ArgFixedTheories], rnm: Option[ArgReplicaRenamer], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
118.  case class DFTheoryEnsembleInstances(nm: Name, fuq: Option[ModForceUnderQuickLoad], tt: Option[ArgTargetTheories], tm: Option[ArgTargetMultiple], ss: Option[ArgEnsembleSorts], cs: Option[ArgEnsembleConsts], ms: Option[ArgMultiples], tic: Option[ArgTheoryInterpretationCheck], ps: Option[ArgPermutations], srs: Option[ArgSpecialRenamings], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
119.  case class DFTheoryEnsembleMultiple(nm: Name, n: Number, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
120.  case class DFTheoryEnsembleOverloadings(nm: Name, ns: ArgNumbers, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
121.  case class DFTheoryInstance(nm: Name, sr: ArgSource, tar: ArgTarget, trans: ArgTranslation, fts: Option[ArgFixedTheories], rnm: Option[ArgRenamer], ntn: Option[ArgNewTranslationName], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
122.  case class DFTheoryProcessors(nm: Name, as: Option[ArgAlgebraicSimplifier], aos: Option[ArgAlgebraicOrderSimplifier], atc: Option[ArgAlgebraicTermComparator], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
123.  case class DFTranslation(n: Name, f: Option[ModForce], fu: Option[ModForceUnderQuickLoad], de: Option[ModDontEnrich], sour: ArgSource, tar: ArgTarget, asms: Option[ArgAssumptions], fxd: Option[ArgFixedTheories], sps: Option[ArgSortPairs], cps: Option[ArgConstPairs], ct: Option[ArgCoreTranslation], tic: Option[ArgTheoryInterpretationCheck], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
124.  class DFTranslationC extends Comp[DFTranslation]
125.  case class DFTransportedSymbols(ns: ArgNameList, tr: ArgTranslation, rn: Option[ArgRenamer], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
126.  trait DefForm extends AnyRef
127.  class DefFormParsers extends AnyRef
128.  case class DefString(s: String, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
129.  case class Define(cont: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
130.  case class EnsembleDontTranslateConst(nm: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
131.  case class Heralding(name: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
132.  case class IMPSApply(f: IMPSMathExp, ts: List[IMPSMathExp]) extends IMPSMathExp with Product with Serializable
133.  case class IMPSAtomSort(s: String) extends IMPSSort with Product with Serializable
134.  case class IMPSBinaryFunSort(s1: IMPSSort, s2: IMPSSort) extends IMPSSort with Product with Serializable
135.  case class IMPSConjunction(ps: List[IMPSMathExp]) extends IMPSMathExp with Product with Serializable
136.  class IMPSDependencyException extends Exception
137.  case class IMPSDisjunction(ps: List[IMPSMathExp]) extends IMPSMathExp with Product with Serializable
138.  case class IMPSDomain(f: IMPSMathExp) extends IMPSQuasiConstructor with Product with Serializable
139.  case class IMPSEquals(t1: IMPSMathExp, t2: IMPSMathExp) extends IMPSMathExp with Product with Serializable
140.  case class IMPSFalseLike(b: IMPSSort) extends IMPSQuasiConstructor with Product with Serializable
141.  case class IMPSFalsehood() extends IMPSMathExp with Product with Serializable
142.  case class IMPSForAll(vs: List[(IMPSVar, IMPSSort)], p: IMPSMathExp) extends IMPSMathExp with Product with Serializable
143.  case class IMPSForSome(vs: List[(IMPSVar, IMPSSort)], p: IMPSMathExp) extends IMPSMathExp with Product with Serializable
144.  case class IMPSIf(p: IMPSMathExp, t1: IMPSMathExp, t2: IMPSMathExp) extends IMPSMathExp with Product with Serializable
145.  case class IMPSIfForm(p: IMPSMathExp, q: IMPSMathExp, r: IMPSMathExp) extends IMPSMathExp with Product with Serializable
146.  case class IMPSIff(p: IMPSMathExp, q: IMPSMathExp) extends IMPSMathExp with Product with Serializable
147.  case class IMPSImplication(p: IMPSMathExp, q: IMPSMathExp) extends IMPSMathExp with Product with Serializable
148.  class IMPSImportTask extends Logger with MMTTask
149.  class IMPSImporter extends Importer
150.  case class IMPSIndividual() extends IMPSMathExp with Product with Serializable
151.  case class IMPSIota(v1: IMPSVar, s1: IMPSSort, p: IMPSMathExp) extends IMPSMathExp with Product with Serializable
152.  case class IMPSIotaP(v1: IMPSVar, s1: IMPSSort, p: IMPSMathExp) extends IMPSMathExp with Product with Serializable
153.  case class IMPSIsDefined(t: IMPSMathExp) extends IMPSMathExp with Product with Serializable
154.  case class IMPSIsDefinedIn(t: IMPSMathExp, s: IMPSSort) extends IMPSMathExp with Product with Serializable
155.  case class IMPSLambda(vs: List[(IMPSVar, IMPSSort)], t: IMPSMathExp) extends IMPSMathExp with Product with Serializable
156.  abstract class IMPSMathExp extends AnyRef
157.  case class IMPSMathSymbol(s: String) extends IMPSMathExp with Product with Serializable
158.  case class IMPSNaryFunSort(ss: List[IMPSSort]) extends IMPSSort with Product with Serializable
159.  case class IMPSNegation(p: IMPSMathExp) extends IMPSMathExp with Product with Serializable
160.  case class IMPSNonVacuous(p: IMPSMathExp) extends IMPSQuasiConstructor with Product with Serializable
161.  case class IMPSQCAppend(s1: IMPSMathExp, s2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
162.  case class IMPSQCBigIntersection(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
163.  case class IMPSQCBigUnion(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
164.  case class IMPSQCCollapse(s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
165.  case class IMPSQCComplement(m: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
166.  case class IMPSQCCons(e: IMPSMathExp, s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
167.  case class IMPSQCConstrict(s: IMPSMathExp, a: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
168.  case class IMPSQCCountableCover(f: IMPSMathExp, a: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
169.  case class IMPSQCDifference(d1: IMPSMathExp, d2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
170.  case class IMPSQCDisjoint(dj1: IMPSMathExp, dj2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
171.  case class IMPSQCDrop(e: IMPSMathExp, s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
172.  case class IMPSQCEmbeds(a: IMPSMathExp, b: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
173.  case class IMPSQCEmptyIndicator(srt: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
174.  case class IMPSQCEmptyIndicatorQ(srt: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
175.  case class IMPSQCEquinumerous(a: IMPSMathExp, b: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
176.  case class IMPSQCFinCard(a: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
177.  case class IMPSQCFinIndic(i: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
178.  case class IMPSQCFinSort(s: IMPSSort) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
179.  case class IMPSQCFiniteCover(f: IMPSMathExp, a: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
180.  case class IMPSQCFirst(s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
181.  case class IMPSQCFseqQ(s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
182.  case class IMPSQCGroups(m: IMPSMathExp, mul: IMPSMathExp, e: IMPSMathExp, inv: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
183.  case class IMPSQCIn(e1: IMPSMathExp, e2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
184.  case class IMPSQCInSeq(s1: IMPSMathExp, s2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
185.  case class IMPSQCIntersection(i1: IMPSMathExp, i2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
186.  case class IMPSQCInvariant(a: IMPSMathExp, f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
187.  case class IMPSQCLength(o: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
188.  case class IMPSQCMBijective(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
189.  case class IMPSQCMBijectiveOn(f: IMPSMathExp, a: IMPSMathExp, b: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
190.  case class IMPSQCMComposition(g: IMPSMathExp, f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
191.  case class IMPSQCMDomain(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
192.  case class IMPSQCMId(s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
193.  case class IMPSQCMImage(f: IMPSMathExp, s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
194.  case class IMPSQCMInjective(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
195.  case class IMPSQCMInjectiveOn(f: IMPSMathExp, a: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
196.  case class IMPSQCMInverse(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
197.  case class IMPSQCMInverseImage(f: IMPSMathExp, v: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
198.  case class IMPSQCMRange(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
199.  case class IMPSQCMRestrict(f: IMPSMathExp, a: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
200.  case class IMPSQCMRestrict2(f: IMPSMathExp, a: IMPSMathExp, b: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
201.  case class IMPSQCMSurjective(f: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
202.  case class IMPSQCMSurjectiveOn(f: IMPSMathExp, a: IMPSMathExp, b: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
203.  case class IMPSQCNil(o: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
204.  case class IMPSQCNonemptyIndicator(srt: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
205.  case class IMPSQCPair(p: IMPSMathExp, q: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
206.  case class IMPSQCPairQ(s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
207.  case class IMPSQCPartitionQ(p: IMPSMathExp, s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
208.  case class IMPSQCPred2Indicator(pred: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
209.  case class IMPSQCSecond(s: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
210.  case class IMPSQCSingleton(n: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
211.  case class IMPSQCSort2Indicator(sort: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
212.  case class IMPSQCSubset(e1: IMPSMathExp, e2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
213.  case class IMPSQCSubsetEQ(e1: IMPSMathExp, e2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
214.  case class IMPSQCSymDifference(sd1: IMPSMathExp, sd2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
215.  case class IMPSQCTakeFirst(l: IMPSMathExp, n: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
216.  case class IMPSQCUnion(u1: IMPSMathExp, u2: IMPSMathExp) extends IMPSUserDefinedQuasiConstructor with Product with Serializable
217.  abstract class IMPSQuasiConstructor extends IMPSMathExp
218.  case class IMPSQuasiEquals(e1: IMPSMathExp, e2: IMPSMathExp) extends IMPSQuasiConstructor with Product with Serializable
219.  case class IMPSSetSort(s: IMPSSort) extends IMPSSort with Product with Serializable
220.  abstract class IMPSSort extends AnyRef
221.  case class IMPSTotal(f: IMPSMathExp, beta: IMPSSort) extends IMPSQuasiConstructor with Product with Serializable
222.  case class IMPSTruth() extends IMPSMathExp with Product with Serializable
223.  case class IMPSUndefined(s: IMPSSort) extends IMPSMathExp with Product with Serializable
224.  case class IMPSUnknownSort(hash: Int) extends IMPSSort with Product with Serializable
225.  abstract class IMPSUserDefinedQuasiConstructor extends IMPSQuasiConstructor
226.  case class IMPSVar(v: String) extends IMPSMathExp with Product with Serializable
227.  case class IMPSWith(vars: List[(IMPSVar, IMPSSort)], expression: IMPSMathExp) extends IMPSMathExp with Product with Serializable
228.  case class LineComment(s: String, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
229.  case class MSpecName(nm: Name, src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
230.  case class MSpecParallel(specs: List[MaceteSpec], src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
231.  case class MSpecRepeat(specs: List[MaceteSpec], src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
232.  case class MSpecSequential(specs: List[MaceteSpec], src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
233.  case class MSpecSeries(specs: List[MaceteSpec], src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
234.  case class MSpecSound(spec1: MaceteSpec, spec2: MaceteSpec, spec3: MaceteSpec, src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
235.  case class MSpecWithoutMinorPremises(spec: MaceteSpec, src: SourceInfo, cmt: CommentInfo) extends MaceteSpec with Product with Serializable
236.  abstract class MaceteSpec extends DefForm
237.  case class ModCancellative(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
238.  case class ModCommutes(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
239.  case class ModDontEnrich(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
240.  case class ModForce(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
241.  case class ModForceUnderQuickLoad(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
242.  case class ModLemma(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
243.  case class ModNull(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
244.  case class ModQuickLoad(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
245.  case class ModReload(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
246.  case class ModReverse(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
247.  case class ModTex(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
248.  case class ModTransportable(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
249.  case class ModUseNumerals(src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
250.  class NEWIMPSParser extends Logger
251.  case class Name(s: String, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
252.  case class Number(n: Int, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
253.  case class ODefString(o: Either[(DefString, Option[IMPSMathExp]), Name], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
254.  case class QCConstantlike(nm: Name, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
255.  case class QDFSpecForm(sclrs: Option[ArgScalars], ops: Option[ArgOperations], usenum: Option[ModUseNumerals], comm: Option[ModCommutes], src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
256.  type Required = Boolean
257.  abstract class SEXP extends AnyRef
258.  case class SEXPAtom(s: String) extends SEXP with Product with Serializable
259.  case class SEXPNested(args: List[SEXP]) extends SEXP with Product with Serializable
260.  case class Script(s: String, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
261.  case class Section(name: String, dependencies: List[Section], files: List[String], jsons: List[String]) extends Product with Serializable
262.  case class Simplog1stWrapper(d: DefForm, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
263.  type SourceInfo = Option[Either[((Int, Int, Int), (Int, Int, Int)), SourceRef]]
264.  case class TeXCorrespondence(scrpt: Script, src: SourceInfo, cmt: CommentInfo) extends DefForm with Product with Serializable
265.  class TheoryEnsemble extends AnyRef
266.  class TranslationState extends AnyRef