Packages

  • package root
    Definition Classes
    root
  • package provingground

    This is work towards automated theorem proving based on learning, using homotopy type theory (HoTT) as foundations and natural language processing.

    This is work towards automated theorem proving based on learning, using homotopy type theory (HoTT) as foundations and natural language processing.

    The implementation of homotopy type theory is split into:

    • the object HoTT with terms, types, functions and dependent functions, pairs etc
    • the package induction with general inductive types and recursion/induction on these.

    The learning package has the code for learning.

    Scala code, including the spire library, is integrated with homotopy type theory in the scalahott package

    We have implemented a functor based approach to translation in the translation package, used for nlp as well as serialization and parsing.

    The library package is contains basic structures implemented in HoTT.

    Definition Classes
    root
  • package andrewscurtis
    Definition Classes
    provingground
  • package examples
    Definition Classes
    provingground
  • package induction

    Much of the richness of HoTT is in the definitions of Inductive types (and their indexed counterparts) and of (dependent) functions on these by recursion and induction These are implemented using several layers of recursive definitions and diagonals (i.e., fixed points).

    Much of the richness of HoTT is in the definitions of Inductive types (and their indexed counterparts) and of (dependent) functions on these by recursion and induction These are implemented using several layers of recursive definitions and diagonals (i.e., fixed points). In HoTT, recursion and induction are applications of (dependent) functions rec_W,X and ind_W, Xs to the definition data.

    It is useful to capture information regarding inductive types and the recursion and induction functions in scala types. Our implementation is designed to do this.

    Inductive Type Definitions

    Inductive types are specified by introduction rules. Each introduction rule is specified in ConstructorShape (without specifying the type) and ConstructorTL including the specific type. The full definition is in ConstructorSeqTL.

    Recursion and Induction functions

    These are defined recursively, first for each introduction rule and then for the inductive type as a whole. A subtlety is that the scala type of the rec_W,X and induc_W, Xs functions depends on the scala type of the codomain X (or family Xs). To make these types visible, some type level calculations using implicits are done, giving traits ConstructorPatternMap and ConstructorSeqMap that have recursive definition of the recursion and induction functions, the former for the case of a single introduction rule. Traits ConstructorSeqMapper and ConstructorPatternMapper provide the lifts.

    Indexed Versions

    There are indexed versions of all these definitions, to work with indexed inductive type families.

    Definition Classes
    provingground
  • package interface
    Definition Classes
    provingground
  • package learning
    Definition Classes
    provingground
  • package library
    Definition Classes
    provingground
  • package scalahott
    Definition Classes
    provingground
  • package scratch
    Definition Classes
    provingground
  • package translation

    Translation primarily using a functorial framework - see Translator$, for natural language processing as well as serialization, formatted output, parsing, interface with formal languages etc.

    Translation primarily using a functorial framework - see Translator$, for natural language processing as well as serialization, formatted output, parsing, interface with formal languages etc.

    Besides the Translator framework and helper typeclasses is Functors, several structures for concrete languages including our implementation of HoTT are in this package.

    Definition Classes
    provingground
  • Base
  • Context
  • FiniteDistribution
  • Frankl
  • HoTT
  • JvmUtils
  • LinearStructure
  • MereProposition
  • PickledWeighted
  • ProbabilityDistribution
  • Subst
  • SubstImplicits
  • TermList
  • TermListImplicits
  • Utils
  • Weighted

object HoTT

Core of Homotopy Type Theory (HoTT) implementation. Includes: - terms : Term, - types : Typ - universes - functions and dependent functions (see [FuncLike], [Func]) - function types FuncTyp and pi-types PiDefn, - lambda definitions LambdaLike, - pairs PairTerm and dependent pairs DepPair - product types ProdTyp and sigma types SigmaTyp - Coproduct types PlusTyp, the Unit type Unit and the empty type Zero - recursion and induction functions for products, coproducts

General inductive types are not implemented here, but in the induction package.

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

Type Members

  1. trait AbsPair[+U <: Term with Subs[U], +V <: Term with Subs[V]] extends Term with Subs[AbsPair[U, V]]

    Abstract pair, parametrized by scala types of components, generally a (dependent) pair object or a product type.

  2. trait AnySym extends AnyRef

    Symbol - may be a name or a formal expression

  3. class ApplnFailException extends IllegalArgumentException
  4. case class ApplnSym[W <: Term with Subs[W], U <: Term with Subs[U]](func: FuncLike[W, U], arg: W) extends AnySym with Product with Serializable

    A symbol representing a formal application

  5. class AtomicSym extends AnySym

    A constant symbol, so a name.

  6. trait AtomicTerm extends Term with Subs[AtomicTerm]

    Objects with simple substitution.

  7. case class AvoidVarFormalException(func: Term, arg: Term, variable: Term) extends Exception with Product with Serializable
  8. case class AvoidVarInvarianceException(variable: Term, term: Term, result: Term) extends Exception with Product with Serializable
  9. trait BaseUniv extends AnyRef

    A universe that is equal (in scala) to Type but may have refined scala type.

  10. class Cnst extends Term

    Just a wrapper to allow singleton objects

  11. class CnstFunc[U <: Term with Subs[U], V <: Term with Subs[V]] extends Cnst with Func[U, V]
  12. class CnstFuncLike[U <: Term with Subs[U], V <: Term with Subs[V]] extends Cnst with FuncLike[U, V]
  13. case class CodomSym(func: AnySym) extends AnySym with Product with Serializable

    Symbol for co-domain of a symbolic function

  14. case class Composition[U <: Term with Subs[U], V <: Term with Subs[V], W <: Term with Subs[W]](f: Func[V, W], g: Func[U, V]) extends Func[U, W] with Subs[Composition[U, V, W]] with Product with Serializable
  15. trait ConstantTerm extends Term

    Term invariant under substitution.

    Term invariant under substitution. Creating a new object from this is not valid.

  16. trait ConstantTyp extends Typ[Term]

    Term invariant under substitution.

    Term invariant under substitution. Creating a new object from this is not valid.

  17. trait DepFunc[W <: Term with Subs[W], U <: Term with Subs[U]] extends FuncLike[W, U]

    a dependent function - rarely used trait as not closed under substitution.

  18. class DepFuncDefn[W <: Term with Subs[W], U <: Term with Subs[U]] extends DepFunc[W, U]

    A dependent function defined by a scala funcion

  19. case class DepPair[W <: Term with Subs[W], U <: Term with Subs[U]](first: W, second: U, fibers: TypFamily[W, U]) extends Term with AbsPair[W, U] with Product with Serializable

    Dependent pair (a: A, b : B(a)) - element of a Sigma type.

  20. case class DepSymbolicFunc[W <: Term with Subs[W], U <: Term with Subs[U]](name: AnySym, fibers: TypFamily[W, U]) extends FuncLike[W, U] with Symbolic with Product with Serializable

    Symbolic dependent function, acts formally.

  21. case class DomSym(func: AnySym) extends AnySym with Product with Serializable

    Symbol for domain of a symbolic function

  22. trait Equality[U <: Term with Subs[U]] extends Term with Subs[Equality[U]]
  23. trait ExstFunc extends AnyRef
  24. trait Func[W <: Term with Subs[W], +U <: Term with Subs[U]] extends FuncLike[W, U] with Subs[Func[W, U]]

    a function (pure, not dependent), i.e., a term in a function type, has a codomain and a fixed type for the domain.

  25. class FuncDefn[W <: Term with Subs[W], U <: Term with Subs[U]] extends Func[W, U]

    A function defined by a scala function

  26. trait FuncLike[W <: Term with Subs[W], +U <: Term with Subs[U]] extends Term with (W) => U with Subs[FuncLike[W, U]]

    Terms that are functions or dependent functions, is a scala function, but the apply is not directly defined - instead the method FuncLike#act is defined.

  27. case class FuncTyp[W <: Term with Subs[W], U <: Term with Subs[U]](dom: Typ[W], codom: Typ[U]) extends GenFuncTyp[W, U] with Typ[Func[W, U]] with Subs[FuncTyp[W, U]] with Product with Serializable

    Function type - pure, not dependent.

  28. abstract class GenFuncTyp[W <: Term with Subs[W], U <: Term with Subs[U]] extends Typ[FuncLike[W, U]] with Subs[GenFuncTyp[W, U]]

    Possibly dependent function type.

    Possibly dependent function type. Meant to override equality so that an object with scala type a Pi-Type but with fiber a constant is equal to the corresponding function type.

  29. case class IdentityTyp[U <: Term with Subs[U]](dom: Typ[U], lhs: U, rhs: U) extends Typ[Equality[U]] with Subs[IdentityTyp[U]] with Product with Serializable

    The identity type.

    The identity type. This is the type lhs = rhs

  30. trait IndInducFuncLike[W <: Term with Subs[W], +U <: Term with Subs[U], F <: Term with Subs[F], IDFT <: Term with Subs[IDFT]] extends FuncLike[W, U]

    common trait for indexed induction functions, for serialization and pretty printing.

  31. trait IndRecFunc[W <: Term with Subs[W], +U <: Term with Subs[U], F <: Term with Subs[F]] extends Func[W, U]

    common trait for indexed recurion functions, for serialization and pretty printing.

  32. trait InducFuncLike[W <: Term with Subs[W], +U <: Term with Subs[U]] extends FuncLike[W, U]

    common trait for induction functions, for serialization and pretty printing.

  33. class InnerSym[U <: Term with Subs[U]] extends AnySym

    A symbol to be used to generate new variables of a type, without changing toString.

  34. case class LambdaFixed[X <: Term with Subs[X], Y <: Term with Subs[Y]](variable: X, value: Y) extends LambdaLike[X, Y] with Func[X, Y] with Subs[LambdaFixed[X, Y]] with Product with Serializable

    lambda which is known to be pure, i.e., have fixed codomain; this is reflected in its scala class; one should usually not use the constructor of this case class, instead use the function lambda or the syntactic sugar for this, e.g.

    lambda which is known to be pure, i.e., have fixed codomain; this is reflected in its scala class; one should usually not use the constructor of this case class, instead use the function lambda or the syntactic sugar for this, e.g. 

    val f = x :-> y

    this creates a new variable to avoid name collisions.

    Note

    that this construction gives a runtime error if the type of y depends on x.

  35. sealed trait LambdaLike[X <: Term with Subs[X], Y <: Term with Subs[Y]] extends FuncLike[X, Y]

    A lambda-expression; variable is mapped to value.

    A lambda-expression; variable is mapped to value. This may or may not be a dependent function. If it is required at compile time that it is not dependent, and hence has scala type Func, then use the class LambdaFixed

    Note

    Equality is overriden here, so that pure functions disguised as dependent ones can be equal to undisguised pure functions.

  36. case class LambdaTerm[X <: Term with Subs[X], Y <: Term with Subs[Y]](variable: X, value: Y) extends LambdaLike[X, Y] with Product with Serializable

    functions given by lambda, which may be dependent; even if it is pure, the scala type does not show this; one should usually not use the constructor of this case class, instead use the function lmbda or the syntactic sugar for this, e.g.

    functions given by lambda, which may be dependent; even if it is pure, the scala type does not show this; one should usually not use the constructor of this case class, instead use the function lmbda or the syntactic sugar for this, e.g. 

    val f = x :~> y

    Note the :~>, not :-> These create a new variable to avoid name collisions.

  37. case class LeftProjSym(name: AnySym) extends AnySym with Product with Serializable

    symbol for left component in pair from a given symbol

  38. case class MereWitness(value: Term) extends AnySym with Product with Serializable
  39. trait MiscAppln extends Term

    record a function as an application, especially for serialization

  40. case class Name(name: String) extends AtomicSym with Product with Serializable

    Strings as symbols

  41. trait NameFactory extends AnyRef
  42. case class NamedDepFunc[W <: Term with Subs[W], +U <: Term with Subs[U]](name: AnySym, func: FuncLike[W, U]) extends FuncLike[W, U] with Product with Serializable

    wrapped dependent function adding name

  43. case class NamedFunc[W <: Term with Subs[W], +U <: Term with Subs[U]](name: AnySym, func: Func[W, U]) extends Func[W, U] with Product with Serializable

    wrapped function adding name

  44. case class NotTypeException(tp: Term) extends IllegalArgumentException with Product with Serializable
  45. case class OptDepFuncDefn[W <: Term with Subs[W]](func: (W) => Option[Term], dom: Typ[W]) extends DepFunc[W, Term] with Subs[OptDepFuncDefn[W]] with Product with Serializable
  46. case class PairTerm[U <: Term with Subs[U], V <: Term with Subs[V]](first: U, second: V) extends AbsPair[U, V] with Subs[PairTerm[U, V]] with Product with Serializable

    Term (a, b) in A times B

  47. case class PiDefn[W <: Term with Subs[W], U <: Term with Subs[U]](variable: W, value: Typ[U]) extends GenFuncTyp[W, U] with Typ[FuncLike[W, U]] with Subs[PiDefn[W, U]] with Product with Serializable

    Pi-Type, defined in terms of a variable and value, i.e., \Pi_{x: X}Q (latex) with x the variable and Q the value

  48. case class PiSymbolicFunc[W <: Term with Subs[W], U <: Term with Subs[U]](name: AnySym, variable: W, value: Typ[U]) extends FuncLike[W, U] with Symbolic with Product with Serializable

    slightly different DepSymbolicFunc is used instead as this causes some tests to fail

  49. case class PlusTyp[U <: Term with Subs[U], V <: Term with Subs[V]](first: Typ[U], second: Typ[V]) extends Typ[Term] with Subs[PlusTyp[U, V]] with Product with Serializable

    coproduct type A + B

  50. case class ProdTyp[U <: Term with Subs[U], V <: Term with Subs[V]](first: Typ[U], second: Typ[V]) extends Typ[PairTerm[U, V]] with AbsPair[Typ[U], Typ[V]] with Subs[ProdTyp[U, V]] with Product with Serializable

    The product type A times B

    The product type A times B

    first

    the first component

    second

    the second component

  51. trait RecFunc[W <: Term with Subs[W], +U <: Term with Subs[U]] extends Func[W, U]

    common trait for recursion functions, for serialization and pretty printing.

  52. case class Refl[U <: Term with Subs[U]](dom: Typ[U], value: U) extends Equality[U] with Subs[Refl[U]] with Product with Serializable

    the reflexivity term with type an equality value = value

  53. implicit class RichTerm[U <: Term with Subs[U]] extends AnyRef

    Operations on terms

  54. case class RightProjSym(name: AnySym) extends AnySym with Product with Serializable

    symbol for right component in pair from a given symbol

  55. case class SigmaTyp[W <: Term with Subs[W], U <: Term with Subs[U]](fibers: TypFamily[W, U]) extends Typ[AbsPair[W, U]] with Subs[SigmaTyp[W, U]] with Product with Serializable

    Sigma Type, i.e., dependent pair type.

  56. trait SmallTyp extends Typ[Term]

    Types with symbolic objects not refined.

  57. trait Subs[+U <: Term] extends AnyRef

    specify result of substitution a typical class is closed under substitution.

  58. case class SymbEquality[U <: Term with Subs[U]](name: AnySym, typ: IdentityTyp[U]) extends Equality[U] with Symbolic with Product with Serializable
  59. case class SymbObj[+U <: Term with Subs[U]](name: AnySym, typ: Typ[U]) extends Term with Symbolic with Product with Serializable

    symbolic objects that are Terms but no more refined ie, not pairs, formal functions etc.

  60. case class SymbProp(name: AnySym) extends Typ[Term] with Symbolic with Product with Serializable

    Symbolic propositions.

    Symbolic propositions. All symbolic objects of this type are witnesses, hence equal.

  61. case class SymbTyp(name: AnySym, level: Int) extends Typ[Term] with Symbolic with Product with Serializable

    Symbolic types, which the compiler knows are types.

  62. trait Symbolic extends Term

    terms that are given (and determined) by name; does not include, for instance, pairs each of whose instance is given by a name; most useful for pattern matching, where the name contains information about formal function applications etc.

  63. case class SymbolicFunc[W <: Term with Subs[W], U <: Term with Subs[U]](name: AnySym, dom: Typ[W], codom: Typ[U]) extends Func[W, U] with Subs[Func[W, U]] with Symbolic with Product with Serializable

    A symbolic function, acts formally.

  64. trait Term extends Subs[Term]

    A HoTT term.

  65. case class TermSymbol(term: Term) extends AnySym with Product with Serializable

    term as a symbol

  66. trait TermSyms extends AnyRef

    Symbols for printing, allowing choice between e.g.

    Symbols for printing, allowing choice between e.g. unicode and plain text

  67. trait Typ[+U <: Term with Subs[U]] extends Term with Subs[Typ[U]]

    HoTT Type; The compiler knows that objects have scala-type extending U.

    HoTT Type; The compiler knows that objects have scala-type extending U. In particular, we can specify that the objects are types, functions, dependent functions etc.

    U

    bound on scala type of objects with this as type. in practice, it is symbolic objects of the type whose scala type is bounded.

  68. type TypFamily[W <: Term with Subs[W], +U <: Term with Subs[U]] = Func[W, Typ[U]]

    type family

  69. type Univ = Typ[Typ[Term]]

    Notation for universes.

  70. case class Universe(level: Int) extends Univ with Subs[Universe] with Product with Serializable

    The (usual) universes

  71. trait Variable[U <: Term with Subs[U]] extends AnyRef

Deprecated Type Members

  1. case class PiTyp[W <: Term with Subs[W], U <: Term with Subs[U]](fibers: TypFamily[W, U]) extends GenFuncTyp[W, U] with Typ[FuncLike[W, U]] with Subs[PiTyp[W, U]] with Product with Serializable

    For all/Product for a type family.

    For all/Product for a type family. This is the type of dependent functions. deprecated in favour of PiDefn

    Annotations
    @deprecated
    Deprecated

    (Since version 14/12/2016) Use PiDefn

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val One: Unit.type
  5. val Type: Universe

    The first universe

  6. def applyFunc(func: Term, arg: Term): Term
  7. def applyFuncOpt(func: Term, arg: Term): Option[Term]
  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. def asLambdas[U <: Term with Subs[U]](term: U): Option[U]
  10. def avoidVar[U <: Term with Subs[U]](t: Term, x: U): U

    returns x after modifying to avoid clashes of variables

  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  12. def composition[U <: Term with Subs[U], V <: Term with Subs[V], W <: Term with Subs[W]](f: Func[V, W], g: Func[U, V]): Composition[U, V, W]

    composition of functions, defined as a lambda

  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  15. def evalSym(symbobj: (AnySym) => Term)(x: Term, y: Term): (AnySym) => Option[Term]
  16. def fold(fn: Term)(args: Term*): Term

    fold using function application after applying functions; used mainly when type information is lost (at runtime).

  17. def foldOpt(fn: Term)(args: Term*): Option[Term]
  18. def foldnames: (Term, List[AnySym]) => Term

    folds in as many terms with names given by the list as possible, applying terms as long as the result is a function and the list is non-empty.

  19. def foldterms: (Term, List[Term]) => Term

    folds in as many terms of the list as possible, applying terms as long as the result is a function and the list is non-empty.

  20. def fromSkolemized(typ: Typ[Term])(y: Term): Term
  21. def funcToLambda[U <: Term with Subs[U], V <: Term with Subs[V]](fn: FuncLike[U, V]): LambdaLike[U, V]

    converts a general function f to a lambda x :-> f(x); if f is already a lambda, returns f without boxing

  22. def funcToLambdaFixed[U <: Term with Subs[U], V <: Term with Subs[V]](fn: Func[U, V]): LambdaFixed[U, V]
  23. def getArg[D <: Term with Subs[D], U <: Term with Subs[U]](func: FuncLike[D, U]): (Term) => Option[D]

    returns Some(x) if the term is of the form f(x) with f given, otherwise None

    returns Some(x) if the term is of the form f(x) with f given, otherwise None

    func

    function f to match for f(x)

  24. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  25. def getName(n: Int): String
  26. def getTypFamily(dom: Term, target: Typ[Term]): Option[Term]
  27. def getTypVariables(n: Int)(t: Term): List[Typ[Term]]
  28. def getVar[U <: Term with Subs[U]](typ: Typ[U])(implicit factory: NameFactory): U

    return variable with name from factory.

  29. def getVariables(n: Int)(t: Term): List[Term]

    returns variab in the term, converting functions to lambdas if needed.

  30. def getVars(t: Term, n: Int): (Vector[Term], Term)
  31. def hasName(sym: AnySym): (Term) => Boolean

    checks if symbolic object has given name.

  32. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  33. def id[U <: Term with Subs[U]](typ: Typ[U]): Func[U, U]

    the identity function defined as a lambda.

  34. var ignoreLevels: Boolean
  35. def instantiate(substitutions: (Term) => Option[Term], target: Typ[Term]): (Term) => Option[Term]

    instantiates variable values in a term if it is made from lambdas, to give a term (if possible) of a required HoTT type.

    instantiates variable values in a term if it is made from lambdas, to give a term (if possible) of a required HoTT type.

    substitutions

    substitutions to make.

    target

    required type after instantiation

  36. def isFunc: (Term) => Boolean

    returns whether term is a function

  37. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  38. def isProp(x: Typ[Term]): Boolean
  39. def isPropFmly(t: Typ[Term]): Boolean
  40. def isTyp: (Term) => Boolean

    returns whether term is a type

  41. def isTypFamily: (Term) => Boolean

    returns whether term is a type family

  42. def isUniv(x: Term): Boolean

    returns whether term is a universe

  43. def isVar(t: Term): Boolean

    returns whether term is a variable

  44. def isWitness(t: Term): Boolean
  45. def lambda[U <: Term with Subs[U], V <: Term with Subs[V]](variable: U)(value: V): FuncLike[U, V]

    constructor for an (in general) dependent lambda; creates a new variable and substitutes this in the value, to avoid name collisions; it is better style to use the syntactic sugar e.g.

    constructor for an (in general) dependent lambda; creates a new variable and substitutes this in the value, to avoid name collisions; it is better style to use the syntactic sugar e.g. 

    val f = x :~> y

    Note the :~>, not :->

  46. def lambdaClosure(vars: Vector[Term])(t: Term): Term

    returns term as a (lambda) function of the variables in vars on which it depends.

  47. def lambdaPair[U <: Term with Subs[U], V <: Term with Subs[V]](variable: U)(value: V): AbsPair[U, V]
  48. def lmbda[U <: Term with Subs[U], V <: Term with Subs[V]](variable: U)(value: V): Func[U, V]

    constructor for a pure lambda, i.e., not a dependent function; this gives a runtime error if the type of the variable depends on the value.

    constructor for a pure lambda, i.e., not a dependent function; this gives a runtime error if the type of the variable depends on the value. creates a new variable and substitutes this in the value, to avoid name collisions; it is better style to use the syntactic sugar e.g. 

    val f = x :-> y
  49. def maxLambda(t: Term): (Vector[Term], Term)
  50. lazy val mkPair: (Term, Term) => AbsPair[Term, Term]

    makes a pair with the appropriate runtime type

  51. def nameCard(s: String): Int
  52. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  53. def negate: (Typ[Term]) => Typ[Term]

    Negation with some simplification

  54. def negateContra(typ: Typ[Term]): Term

    Proof of A -> negate(A) -> Zero

  55. def nextChar(s: Iterable[Char]): Char

    Symbol factory

  56. def nextName(name: String): String
  57. def nextVar(s: Iterable[Term])(typ: Typ[Term]): Term

    get variable from symbol factory

  58. def nextVar(typ: Typ[Term], vars: Vector[Term], prefix: String = "@"): Term
  59. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  60. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  61. def optlambda(variable: Term): (Term) => Term

    lambda if necessary, otherwise constant.

  62. def outerSym(sym: Symbolic): Symbolic

    Unwraps symbols if they are wrapped - wrapping typical happens in lambdas.

  63. def pair[U <: Term with Subs[U], V <: Term with Subs[V]](first: Typ[U] with Subs[Typ[U]], second: Typ[V] with Subs[Typ[V]]): ProdTyp[U, V]

    overloaded method returning a pair object or a pair type.

  64. def pair[U <: Term with Subs[U], V <: Term with Subs[V]](first: U, second: V): PairTerm[U, V]

    overloaded method returning a pair object or a pair type.

  65. def partialLambdaClosures(vars: Vector[Term])(t: Term): Vector[Term]

    returns all partial lambda closures

  66. def pi[U <: Term with Subs[U], V <: Term with Subs[V]](variable: U)(value: Typ[V]): Typ[FuncLike[U, V]]

    lambda-like syntax for piDefn

  67. def piClosure(vars: Vector[Term])(t: Typ[Term]): Typ[Term]

    returns type as a Pi-Type of the variables in vars on which it depends.

  68. def piDefn[U <: Term with Subs[U], V <: Term with Subs[V]](variable: U)(value: Typ[V]): PiDefn[U, V]

    constructor for pi-Types; creates a new variable and substitutes this in the value, to avoid name collisions; it is better style to use the syntactic sugar e.g.

    constructor for pi-Types; creates a new variable and substitutes this in the value, to avoid name collisions; it is better style to use the syntactic sugar e.g. 

    val P = x ~>: A

    Note the ~>:, not ->:

  69. def polyLambda(variables: List[Term], value: Term): Term

    repeatedly apply lambda

  70. def prefixedNextName(fullname: String): String
  71. def replaceVar[U <: Term with Subs[U]](variable: U)(x: Term, y: Term): U with Subs[U]
  72. val resizedEqual: (Typ[Term], Typ[Term]) => Boolean
  73. def sigma[U <: Term with Subs[U], V <: Term with Subs[V]](variable: U)(value: Typ[V]): Typ[AbsPair[U, V]]

    Sigma type defined using lmbda, so with new variable created.

  74. def skipApply(f: Term, x: Term, n: Int): Option[Term]
  75. def skipVars(t: Term, n: Int): Option[Term]
  76. val skolemize: (Typ[Term]) => Typ[Term]
  77. def symSubs[U <: Term](symbobj: (AnySym) => U)(x: Term, y: Term): (AnySym) => U

    substitute symbols, with the only non-trivial substitution for formal applications.

  78. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  79. def termSymbol(term: Term): AnySym
  80. def toString(): String
    Definition Classes
    AnyRef → Any
  81. def toTyp(t: Term): Typ[U] forSome {type U <: Term with Subs[U]}
  82. def toTypOpt(t: Term): Option[Typ[U] forSome {type U <: Term with Subs[U]}]
  83. def typFamilyDepth: (Term) => Option[Int]
  84. def typFamilyTarget: (Term) => Option[Typ[Term]]
  85. def typOpt(x: Term): Option[Typ[Term]]
  86. def univlevel: (Typ[Typ[Term]]) => Int
  87. def usedChars(s: Iterable[Term]): Iterable[Char]

    Helper for symbol factory

  88. def vacuous[U <: Term with Subs[U]](codom: Typ[U]): Func[Term, U]

    Map from 0 to A.

  89. def vartyp[U <: Term with Subs[U]](t: U)(implicit arg0: Variable[U]): Typ[U]
  90. var verbose: Boolean
  91. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  92. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  93. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  94. def witVar[U <: Term with Subs[U]](t: U): U
  95. object AbsPair
  96. object ApplnFailException extends Serializable
  97. implicit object DefaultNameFactory extends NameFactory

    factory for variable names

  98. object ExstFunc
  99. object Fold

    convenience methods to apply methods of special scala types such as functions without the compiler knowing that the object has the special type.

  100. object FormalAppln

    Pattern matching for a formal application.

  101. case object HashSym extends AtomicSym with Product with Serializable
  102. object IdentityTyp extends Serializable
  103. object InnerSym
  104. object MiscAppln
  105. object Name extends Serializable
  106. object NamedTerm
  107. object PiDefn extends Serializable
  108. object PlusTyp extends Serializable
  109. object ProdTyp extends Serializable
  110. case object Prop extends BaseUniv with Univ with Product with Serializable
  111. object Sgma
  112. object SigmaTyp extends Serializable
  113. object SimpleSyms extends TermSyms

    plain text symbols for maps etc.

  114. case object Star extends AtomicTerm with Product with Serializable

    the object in the Unit type

  115. object Subs
  116. object Tuple
  117. object UnicodeSyms extends TermSyms

    unicode symbols for maps etc.

  118. case object Unit extends SmallTyp with Product with Serializable

    Unit type.

  119. object Variable
  120. case object Zero extends SmallTyp with Product with Serializable

    Empty type

  121. case object vacuousSym extends AtomicSym with Product with Serializable

    Symbol for map 0 -> A

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped