Packages

case class HoTTParser(ctx: Context = Context.Empty, contextMap: Map[String, Context] = Map()) extends Product with Serializable

Self Type
HoTTParser
Linear Supertypes
Serializable, Product, Equals, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. HoTTParser
  2. Serializable
  3. Product
  4. Equals
  5. AnyRef
  6. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new HoTTParser(ctx: Context = Context.Empty, contextMap: Map[String, Context] = Map())

Value Members

  1. def +(exp: Expr): HoTTParser
  2. def +(dfn: Defn): HoTTParser
  3. def +(n: String, t: Term): HoTTParser
  4. def addImport(s: String): HoTTParser
  5. def alphachar[_](implicit arg0: P[Any]): ParsingRun[Unit]
  6. def alphanum[_](implicit arg0: P[Any]): P[Unit]
  7. def applnP[_](implicit arg0: P[Any]): P[Term]
  8. def block[_](implicit arg0: P[Any]): P[Block]
  9. def break[_](implicit arg0: P[Any]): P[Unit]
  10. def context[_](implicit arg0: P[Any]): P[Context]
  11. val contextMap: Map[String, Context]
  12. val ctx: Context
  13. def defn[_](implicit arg0: P[Any]): P[Defn]
  14. def expr[_](implicit arg0: P[Any]): P[Expr]
  15. def funcTyp[_](implicit arg0: P[Any]): ParsingRun[FuncTyp[U, U] forSome {type U <: Term with Subs[U], type U <: Term with Subs[U]}]
  16. def imp[_](implicit arg0: P[Any]): P[Import]
  17. def inducP[_](implicit arg0: P[Any]): P[Term]
  18. def lambdaP[_](implicit arg0: P[Any]): P[Term]
  19. def lmbdaP[_](implicit arg0: P[Any]): P[Term]
  20. def name[_](implicit arg0: P[Any]): P[String]
  21. def named[_](implicit arg0: P[Any]): P[Term]
  22. def num[_](implicit arg0: P[Any]): P[scalahott.NatRing.LocalTerm with Subs[scalahott.NatRing.LocalTerm]]
  23. def parens[_](implicit arg0: P[Any]): P[Term]
  24. def parseBlock(txt: String): Parsed[Block]
  25. def parseContext(txt: String): Parsed[Context]
  26. def piTyp[_](implicit arg0: P[Any]): ParsingRun[GenFuncTyp[Term, U] forSome {type U <: Term with Subs[U]}]
  27. def plusTyp[_](implicit arg0: P[Any]): ParsingRun[PlusTyp[U, U] forSome {type U <: Term with Subs[U], type U <: Term with Subs[U]}]
  28. def polyApplnP[_](implicit arg0: P[Any]): P[Term]
  29. def predefs[_](implicit arg0: P[Any]): P[Term]
  30. def prodTyp[_](implicit arg0: P[Any]): ParsingRun[ProdTyp[U, U] forSome {type U <: Term with Subs[U], type U <: Term with Subs[U]}]
  31. def productElementNames: Iterator[String]
    Definition Classes
    Product
  32. def recP[_](implicit arg0: P[Any]): P[Term]
  33. def sigmaTyp[_](implicit arg0: P[Any]): ParsingRun[SigmaTyp[Term, U] forSome {type U <: Term with Subs[U]}]
  34. def simpleterm[_](implicit arg0: P[Any]): P[Term]
  35. def spc[_](implicit arg0: P[Any]): P[Unit]
  36. def stat[_](implicit arg0: P[Any]): P[Stat]
  37. def str[_](implicit arg0: P[Any]): P[String]
  38. def symbolic[_](implicit arg0: P[Any]): P[Term]
  39. def term[_](implicit arg0: P[Any]): P[Term]