< Back

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
object HoTT
Core of Homotopy Type Theory (HoTT) implementation.
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.
Definition Classes
provingground
AbsPair
AnySym
ApplnFailException
ApplnSym
AtomicSym
AtomicTerm
AvoidVarFormalException
AvoidVarInvarianceException
BaseUniv
Cnst
CnstFunc
CnstFuncLike
CodomSym
Composition
ConstantTerm
ConstantTyp
DefaultNameFactory
DepFunc
DepFuncDefn
DepPair
DepSymbolicFunc
DomSym
Equality
ExstFunc
Fold
FormalAppln
Func
FuncDefn
FuncLike
FuncTyp
GenFuncTyp
HashSym
IdentityTyp
IndInducFuncLike
IndRecFunc
InducFuncLike
InnerSym
LambdaFixed
LambdaLike
LambdaTerm
LeftProjSym
MereWitness
MiscAppln
Name
NameFactory
NamedDepFunc
NamedFunc
NamedTerm
NotTypeException
OptDepFuncDefn
PairTerm
PiDefn
PiSymbolicFunc
PiTyp
PlusTyp
ProdTyp
Prop
RecFunc
Refl
RichTerm
RightProjSym
Sgma
SigmaTyp
SimpleSyms
SmallTyp
Star
Subs
SymbEquality
SymbObj
SymbProp
SymbTyp
Symbolic
SymbolicFunc
Term
TermSymbol
TermSyms
Tuple
Typ
UnicodeSyms
Unit
Universe
Variable
Zero
vacuousSym

o

provingground.HoTT

Fold

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.

Linear Supertypes

Ordering

Alphabetic
By Inheritance

Inherited

Fold
AnyRef
Any

Hide All
Show All

Visibility

Public
Protected

Type Members

implicit class Folder[U <: Term with Subs[U]] extends AnyRef

Value Members

final def !=(arg0: Any): Boolean
Definition Classes
AnyRef → Any
final def ##: Int
Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean
Definition Classes
AnyRef → Any
final def asInstanceOf[T0]: T0
Definition Classes
Any
def clone(): AnyRef
Attributes
protected[lang]
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
def defnData: (Term) => Vector[Term]
def domain: (Term) => Typ[Term]
final def eq(arg0: AnyRef): Boolean
Definition Classes
AnyRef
def equals(arg0: AnyRef): Boolean
Definition Classes
AnyRef → Any
final def getClass(): Class[_ <: AnyRef]
Definition Classes
AnyRef → Any
Annotations
@native() @HotSpotIntrinsicCandidate()
def hashCode(): Int
Definition Classes
AnyRef → Any
Annotations
@native() @HotSpotIntrinsicCandidate()
final def isInstanceOf[T0]: Boolean
Definition Classes
Any
final def ne(arg0: AnyRef): Boolean
Definition Classes
AnyRef
final def notify(): Unit
Definition Classes
AnyRef
Annotations
@native() @HotSpotIntrinsicCandidate()
final def notifyAll(): Unit
Definition Classes
AnyRef
Annotations
@native() @HotSpotIntrinsicCandidate()
final def synchronized[T0](arg0: => T0): T0
Definition Classes
AnyRef
def toString(): String
Definition Classes
AnyRef → Any
def value: (Term) => Term
def variable: (Term) => Term
final def wait(arg0: Long, arg1: Int): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException])
final def wait(arg0: Long): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException]) @native()
final def wait(): Unit
Definition Classes
AnyRef
Annotations
@throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

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

Inherited from AnyRef

Inherited from Any

Ungrouped