Type Members

1.  case class ABS(uri: URI, mod: theoryexpr) extends theoryexpr with Product with Serializable
2.  case class APPLY(id: String, sort: String, tms: List[term]) extends term with Product with Serializable
3.  case class AXIOM(uri: URI, as: String, components: List[CoqEntry]) extends theorystructure with Product with Serializable
4.  case class BodyXML(e: CoqEntry) extends CoqXml with Product with Serializable
5.  case class CAST(id: String, sort: String, tm: term, _type: _type) extends term with Product with Serializable
6.  case class CHILD(uri: URI, components: List[CoqEntry]) extends theorystructure with Product with Serializable
7.  case class COFIX(noFun: Int, id: String, sort: String, cofixFunctions: List[CofixFunction]) extends term with Product with Serializable
8.  case class CONST(uri: URI, id: String, sort: String) extends term with objectOccurence with Product with Serializable
9.  case class CofixFunction(id: String, name: String, _type: _type, body: body) extends CoqEntry with Product with Serializable
10.  case class ConstantBody(_for: URI, params: List[String], id: String, body: term) extends CoqEntry with Product with Serializable
11.  case class ConstantType(name: String, params: List[String], id: String, _type: term) extends CoqEntry with Product with Serializable
12.  case class Constraints(e: List[CoqEntry]) extends CoqXml with Product with Serializable
13.  case class Constructor(name: String, _type: term) extends CoqEntry with Product with Serializable
14.  trait CoqEntry extends AnyRef
15.  trait CoqXml extends CoqEntry
16.  case class DEFINITION(uri: URI, as: String, components: List[CoqEntry]) extends theorystructure with Product with Serializable
17.  case class ExprXML(e: theoryexpr) extends CoqXml with Product with Serializable
18.  case class FIX(noFun: Int, id: String, sort: String, fixFunctions: List[FixFunction]) extends term with Product with Serializable
19.  case class FUNAPP(f: theoryexpr, args: List[theoryexpr]) extends theoryexpr with Product with Serializable
20.  case class FixFunction(name: String, id: String, recIndex: Int, _type: _type, body: body) extends CoqEntry with Product with Serializable
21.  case class InductiveDefinition(noParams: Int, params: List[String], id: String, tps: List[InductiveType]) extends CoqEntry with Product with Serializable
22.  case class InductiveType(name: String, inductive: Boolean, id: String, arity: arity, constructors: List[Constructor]) extends CoqEntry with Product with Serializable
23.  case class InnerTypes(of: URI, _types: List[TYPE]) extends CoqEntry with Product with Serializable
24.  case class LAMBDA(sort: String, decls: List[decl], target: target) extends term with Product with Serializable
25.  case class LETIN(sort: String, defs: List[_def], target: target) extends term with Product with Serializable
26.  case class MODULE(uri: URI, params: List[(String, List[CoqXml])], as: String, components: List[theorystructure], componentsImpl: List[theorystructure], attributes: List[CoqXml], attributesImpl: List[CoqXml]) extends theorystructure with Product with Serializable
27.  case class MODULEExpr(uri: URI, params: List[(String, List[CoqXml])], as: String, components: List[CoqXml], children: List[CHILD]) extends theorystructure with Product with Serializable
28.  case class MREF(uri: URI) extends theoryexpr with Product with Serializable
29.  case class MUTCASE(uriType: URI, noType: Int, id: String, sort: String, patternsType: patternsType, inductiveTerm: inductiveTerm, patterns: List[pattern]) extends term with Product with Serializable
30.  case class MUTCONSTRUCT(uri: URI, noType: Int, noConstr: Int, id: String, sort: String) extends term with objectOccurence with Product with Serializable
31.  case class MUTIND(uri: URI, noType: Int, id: String) extends term with objectOccurence with Product with Serializable
32.  case class PROD(_type: String, decls: List[decl], target: target) extends term with Product with Serializable
33.  case class PROJ(uri: URI, noType: Int, id: String, sort: String, tm: term) extends term with Product with Serializable
34.  case class REL(value: Int, binder: String, id: String, idref: String, sort: String) extends term with Product with Serializable
35.  case class Requirement(uri: URI) extends theorystructure with Product with Serializable
36.  case class SECTION(uri: URI, statements: List[theorystructure]) extends theorystructure with Product with Serializable
37.  case class SORT(value: String, id: String) extends term with Product with Serializable
38.  case class SupXML(e: supertypes) extends CoqXml with Product with Serializable
39.  case class THDEF(relUri: URI, df: term) extends theoryexpr with Product with Serializable
40.  case class THEOREM(uri: URI, as: String, components: List[CoqEntry]) extends theorystructure with Product with Serializable
41.  case class TYPE(of: String, tp: term) extends CoqEntry with Product with Serializable
42.  case class TopXML(e: CoqEntry) extends CoqXml with Product with Serializable
43.  case class TranslationState(controller: Controller, toMPath: (URI) ⇒ MPath, toGlobalName: (URI) ⇒ GlobalName, currentT: AbstractTheory) extends Product with Serializable
44.  case class TypesXML(e: CoqEntry) extends CoqXml with Product with Serializable
45.  case class VAR(uri: URI, id: String, sort: String) extends term with objectOccurence with Product with Serializable
46.  case class VARIABLE(uri: URI, as: String, components: List[CoqEntry]) extends theorystructure with Product with Serializable
47.  case class Variable(name: String, params: List[String], id: String, body: Option[body], _type: _type) extends CoqEntry with Product with Serializable
48.  case class WITH(a: theoryexpr, d: theoryexpr) extends theoryexpr with Product with Serializable
49.  case class _def(id: String, sort: String, binder: String, _vardef: term) extends CoqEntry with Product with Serializable
50.  case class _type(tm: term) extends CoqEntry with Product with Serializable
51.  case class arg(relUri: URI, arg: term) extends CoqEntry with Product with Serializable
52.  case class arity(tm: term) extends CoqEntry with Product with Serializable
53.  case class body(tm: term) extends CoqEntry with Product with Serializable
54.  case class decl(id: String, _type: String, binder: String, _vartype: term) extends CoqEntry with Product with Serializable
55.  case class inductiveTerm(tm: term) extends CoqEntry with Product with Serializable
56.  case class instantiate(id: String, oo: objectOccurence, args: List[arg]) extends term with Product with Serializable
57.  trait objectOccurence extends term
58.  case class pattern(tm: term) extends CoqEntry with Product with Serializable
59.  case class patternsType(tm: term) extends CoqEntry with Product with Serializable
60.  case class supertypes(ls: List[CoqEntry]) extends CoqXml with Product with Serializable
61.  case class target(tm: term) extends CoqEntry with Product with Serializable
62.  trait term extends CoqEntry
63.  trait theoryexpr extends CoqEntry
64.  trait theorystructure extends CoqEntry