Packages

object TermPatterns

Patterns, in the sense of Translator.Pattern, as well as some builders for various kinds of HoTT terms. Includes matching recursively and inductively defined functions.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TermPatterns
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. val absPair: Pattern[Term, II]

    matches all pairs

  2. def buildIndDef(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, Term, _]] = (_) => None): (Term, (Term, Vector[Term])) => Option[Term]

    returns inductively defined function as function of domain, codomain and definition data

    returns inductively defined function as function of domain, codomain and definition data

    inds

    inductive types defined (other than products etc)

  3. def buildIndIndDef(inds: (Term) => Option[IndexedConstructorSeqDom[_, Term, _, _, _]] = (_) => None): (Vector[Term], (Term, (Term, Vector[Term]))) => Option[Term]

    returns indexed inductively defined function as function of domain, codomain and definition data

    returns indexed inductively defined function as function of domain, codomain and definition data

    inds

    inductive types defined (other than equality)

  4. def buildIndRecDef(inds: (Term) => Option[IndexedConstructorSeqDom[_, Term, _, _, _]] = (_) => None): (Vector[Term], (Term, (Term, Vector[Term]))) => Option[Term]

    returns indexed recursively defined function as function of domain, codomain and definition data

    returns indexed recursively defined function as function of domain, codomain and definition data

    inds

    indexed inductive types defined (other than equality)

  5. def buildRecDef(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, _, _]] = (_) => None): (Term, (Term, Vector[Term])) => Option[Term]

    returns recursively defined function as function of domain, codomain and definition data

    returns recursively defined function as function of domain, codomain and definition data

    inds

    inductive types defined (other that products etc)

  6. val depPairTerm: Pattern[Term, III]
  7. val equation: Pattern[Term, II]

    matches identity (equality) type, returns lhs and rhs

  8. val firstIncl: Pattern[Term, II]

    matches i_1(a), the first inclusion function, returns the type and value

  9. def fm[U <: Term with Subs[U]](dom: Typ[U], fmly: Term): Func[U, Typ[_]] forSome {type _ <: Term with Subs[_]}
  10. val foldedTerm: Pattern[Term, IV]
  11. val formalAppln: Pattern[Term, II]

    matches formal applications

  12. val funcTyp: Pattern[Term, II]

    matches function types, returning domain and codomain

  13. def getName(sym: AnySym): Option[Name]
  14. val hashSymbolic: Pattern[Term, Named]
  15. val identityTyp: Pattern[Term, III]

    matches identity (equality) type, returns domain, lhs and rhs

  16. val indInducFunc: Pattern[Term, IVIIV]

    matches indexed inductively defined function, returns index, domain, codomain and definition data

  17. val indRecFunc: Pattern[Term, IVIIV]

    matches idexed recursively defined function, returns index, domain, codomain and definition data

  18. val inducFunc: Pattern[Term, IIV]

    matches inductively defined function, returns domain, codomain and definition data

  19. def inducFuncApplied(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, Term, _]]): Pattern[Term, Id]
  20. val introIndInducFunc: Pattern[Term, VIVIIV]
  21. val introIndRecFunc: Pattern[Term, VIVIIV]
  22. val introInducFunc: Pattern[Term, VIIV]
  23. val introRecFunc: Pattern[Term, VIIV]
  24. val lambdaAppln: Pattern[Term, II]

    matches lambda definitions

  25. val lambdaFixedTriple: Pattern[Term, III]
  26. val lambdaTriple: Pattern[Term, III]

    matches lambda applications and returns HoTT-type of the variable as well

  27. val mereWitness: Pattern[Term, II]
  28. val miscAppln: Pattern[Term, II]
  29. val natAddMorph: Pattern[Term, II]
  30. val natLiteral: Pattern[Term, N]
  31. val natProd: Pattern[Term, Un]
  32. val natSucc: Pattern[Term, Un]
  33. val natSum: Pattern[Term, Un]
  34. val natTyp: Pattern[Term, Un]
  35. val natUniv: Pattern[Term, Un]
  36. val natZero: Pattern[Term, Un]
  37. def numberedSymbolic(prefix: String): Pattern[Term, Numbered]
  38. val pairTerm: Pattern[Term, II]
  39. val piLam: Pattern[Term, II]

    matches Pi-Type and returns the fibre as a lambda

  40. val piTriple: Pattern[Term, III]

    matches Pi-Types, returns in the pi-lambda form with the HoTT-type of variable included.

  41. val piTyp: Pattern[Term, Id]

    matches Pi-Type and returns the fibre

  42. val plusTyp: Pattern[Term, II]

    matches coproduct type

  43. val prodTyp: Pattern[Term, II]

    matches product types

  44. val prop: Pattern[Term, Un]

    matches Prop, the false type, returns () : Unit if matched

  45. val propUniv: Pattern[Term, Un]
  46. val recFunc: Pattern[Term, IIV]

    matches recursively defined function, returns domain, codomain and definition data

  47. def recFuncApplied(inds: (Typ[Term]) => Option[ConstructorSeqTL[_, _, _]]): Pattern[Term, Id]
  48. val refl: Pattern[Term, II]
  49. val secondIncl: Pattern[Term, II]

    matches i_2(a), the second inclusion function, returns the type and value

  50. val sigmaLam: Pattern[Term, II]

    matches Sigma-Type and returns fibre as lambda

  51. val sigmaTriple: Pattern[Term, III]

    matches Sigma-Types, returns in the pi-lambda form with the HoTT-type of variable included.

  52. val sigmaTyp: Pattern[Term, Id]

    matches Sigma-Type and returns the fibre

  53. val star: Pattern[Term, Un]

    matches Star, the only element of the true type Unit, returns () : Unit if matched

  54. val stringRep: Pattern[Term, S]
  55. val symName: Pattern[Term, S]

    matches a symbolic name, perhaps wrapped in InnerSym, returns the name as a String

  56. val symString: Pattern[Term, S]
  57. val symbolic: Pattern[Term, Named]

    matches a symbolic name, perhaps wrapped in InnerSym, returns Name

  58. def termToExpr[E](univ: (Int) => Option[E])(implicit arg0: ExprLang[E]): OrElse[Term, E]
  59. def termToExprRaw[E](implicit arg0: ExprLang[E]): OrElse[Term, E]
  60. val unit: Pattern[Term, Un]

    matches the true type Unit, returns () : Unit if matched

  61. val universe: Pattern[Term, N]

    matches Universe(n), returns the level n

  62. val zero: Pattern[Term, Un]

    matches Zero, the false type, returns () : Unit if matched