Packages

case class RepSymbObj[A, +U <: RepTerm[A] with Subs[U]](name: AnySym, typ: Typ[U]) extends RepTerm[A] with Symbolic with Product with Serializable

Linear Supertypes
Serializable, Product, Equals, Symbolic, RepTerm[A], Term, Subs[RepTerm[A]], AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. RepSymbObj
  2. Serializable
  3. Product
  4. Equals
  5. Symbolic
  6. RepTerm
  7. Term
  8. Subs
  9. AnyRef
  10. Any
Implicitly
  1. by ScalaTerm
  2. by any2stringadd
  3. by StringFormat
  4. by Ensuring
  5. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new RepSymbObj(name: AnySym, typ: Typ[U])

Value Members

  1. def dependsOn(that: Term): Boolean

    returns whether this depends on that

    returns whether this depends on that

    Definition Classes
    Term
  2. def equals(that: Any): Boolean
    Definition Classes
    Symbolic → AnyRef → Any
  3. lazy val hashCode: Int
    Definition Classes
    Symbolic → AnyRef → Any
  4. def indepOf(that: Term): Boolean

    returns whether this is independent of that.

    returns whether this is independent of that.

    Definition Classes
    Term
  5. val name: AnySym
    Definition Classes
    RepSymbObj → Symbolic
  6. def newobj: RepSymbObj[A, U]

    A new object with the same type, to be used in place of a variable to avoid name clashes.

    A new object with the same type, to be used in place of a variable to avoid name clashes. Should throw exception when invoked for constants.

    Definition Classes
    RepSymbObj → Subs
  7. def productElementNames: Iterator[String]
    Definition Classes
    Product
  8. def replace(x: Term, y: Term): RepTerm[A] with Subs[RepTerm[A]]

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.

    Definition Classes
    Subs
  9. def subs(x: Term, y: Term): RepTerm[A]

    substitute x by y recursively in this.

    substitute x by y recursively in this.

    Definition Classes
    RepSymbObj → Subs
  10. def term: U
    Implicit
    This member is added by an implicit conversion from RepSymbObj[A, U] toScalaTerm[U, RepSymbObj[A, U]] performed by method ScalaTerm in provingground.scalahott.ScalaRep.This conversion will take place only if an implicit value of type ScalaRep[U, RepSymbObj[A, U]] is in scope.
    Definition Classes
    ScalaTerm
  11. def toString(): String
    Definition Classes
    Symbolic → AnyRef → Any
  12. val typ: Typ[U]

    the HoTT-type of the term

    the HoTT-type of the term

    Definition Classes
    RepSymbObj → RepTerm → Term
  13. def usesVar(t: Term): Boolean

    returns whether the variable t is used as a variable in a lambda definition.

    returns whether the variable t is used as a variable in a lambda definition.

    Definition Classes
    Term