case class ParGenNodes(tg: TermGenParams) extends TermGeneratorNodes[ParMapState] with Product with Serializable
- Alphabetic
- By Inheritance
- ParGenNodes
- Serializable
- Product
- Equals
- TermGeneratorNodes
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new ParGenNodes(tg: TermGenParams)
Type Members
- case class FoldFuncTargetNode(typ: Typ[Term]) extends (Term) => Option[GeneratorNode[Term]] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case class TargetInducFuncsFolded(target: Typ[Term]) extends (ExstInducDefn) => Option[GeneratorNode[Term]] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- Implicit
- This member is added by an implicit conversion from ParGenNodes toany2stringadd[ParGenNodes] performed by method any2stringadd in scala.Predef.
- Definition Classes
- any2stringadd
- def ->[B](y: B): (ParGenNodes, B)
- Implicit
- This member is added by an implicit conversion from ParGenNodes toArrowAssoc[ParGenNodes] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @inline()
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val applnByArgNode: FiberProductMap[Term, ExstFunc, Typ[Term], Term]
function application to get terms by choosing an argument and then a function with domain containing this.
function application to get terms by choosing an argument and then a function with domain containing this.
- Definition Classes
- TermGeneratorNodes
- val applnNode: FiberProductMap[ExstFunc, Term, Typ[Term], Term]
function application to get terms by choosing a function and then a term in its domain
function application to get terms by choosing a function and then a term in its domain
- Definition Classes
- TermGeneratorNodes
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- val backwardTypNodeFamily: BasePiOpt[::[Typ[Term], HNil], Term]
nodes combining backward reasoning targeting types that are (dependent) function types, aggregated over all types
nodes combining backward reasoning targeting types that are (dependent) function types, aggregated over all types
- Definition Classes
- TermGeneratorNodes
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- val curryBackwardTypNodeFamily: BasePiOpt[::[Typ[Term], HNil], Term]
nodes combining backward reasoning targeting types that are (dependent) function types, with domain product, sigma-types or co-products aggregated over all types
nodes combining backward reasoning targeting types that are (dependent) function types, with domain product, sigma-types or co-products aggregated over all types
- Definition Classes
- TermGeneratorNodes
- def curryForTyp(typ: Typ[Term]): Option[GeneratorNode[Term]]
node for targeting functions on products by currying, and also on sigma-types and co-products
node for targeting functions on products by currying, and also on sigma-types and co-products
- Definition Classes
- TermGeneratorNodes
- def ensuring(cond: (ParGenNodes) => Boolean, msg: => Any): ParGenNodes
- Implicit
- This member is added by an implicit conversion from ParGenNodes toEnsuring[ParGenNodes] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: (ParGenNodes) => Boolean): ParGenNodes
- Implicit
- This member is added by an implicit conversion from ParGenNodes toEnsuring[ParGenNodes] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean, msg: => Any): ParGenNodes
- Implicit
- This member is added by an implicit conversion from ParGenNodes toEnsuring[ParGenNodes] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- def ensuring(cond: Boolean): ParGenNodes
- Implicit
- This member is added by an implicit conversion from ParGenNodes toEnsuring[ParGenNodes] performed by method Ensuring in scala.Predef.
- Definition Classes
- Ensuring
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def foldFuncNode(t: Term, depth: Int): GeneratorNode[Term]
Node for folding a function (or term) with a speficied number of arguments to get terms.
Node for folding a function (or term) with a speficied number of arguments to get terms.
- Definition Classes
- TermGeneratorNodes
- def foldFuncTargetNode(t: Term, target: Typ[Term], output: RandomVar[Term]): Option[GeneratorNode[Term]]
Node for folding a function (or term) with a speficied target type to optionally get terms with the target type.
Node for folding a function (or term) with a speficied target type to optionally get terms with the target type.
- Definition Classes
- TermGeneratorNodes
- def foldTypFamily(w: Term): GeneratorNode[Typ[Term]]
Node for fully folding a type family to get types
Node for fully folding a type family to get types
- Definition Classes
- TermGeneratorNodes
- def foldedTargetFunctionNode(typ: Typ[Term]): FlatMapOpt[Term, Term]
Node for generating terms of a type (if possible) by multiple applications of functions tageting the type.
Node for generating terms of a type (if possible) by multiple applications of functions tageting the type.
- Definition Classes
- TermGeneratorNodes
- def formatted(fmtstr: String): String
- Implicit
- This member is added by an implicit conversion from ParGenNodes toStringFormat[ParGenNodes] performed by method StringFormat in scala.Predef.
- Definition Classes
- StringFormat
- Annotations
- @inline()
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def indexedInducIdNode(typF: Typ[Term]): Map[Typ[Term], Typ[Term]]
Start of an indexed introduction rule by fully applying a type family
Start of an indexed introduction rule by fully applying a type family
- typF
the type family for the inductive type
- returns
distribution of types
- Definition Classes
- TermGeneratorNodes
- def indexedIterFuncIsle(targetTyp: Term)(typ: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
Extending indexed introduction rule by an iterated function ending in the inductive type family fully applied.
Extending indexed introduction rule by an iterated function ending in the inductive type family fully applied.
- typ
the type by which we are extending
- returns
distribution on types.
- Definition Classes
- TermGeneratorNodes
- def indexedIterFuncNode(targetTyp: Term): FlatMap[Typ[Term], Typ[Term]]
Aggregating extending indexed introduction rule by iterated function type eding in fully applied inductive type family.
Aggregating extending indexed introduction rule by iterated function type eding in fully applied inductive type family.
- returns
distribution on types.
- Definition Classes
- TermGeneratorNodes
- def indexedIterHeadNode(inductiveTyp: Term): FlatMap[Typ[Term], Typ[Term]]
Aggregating extending introduction types for indexed inductive types by iterated function types
Aggregating extending introduction types for indexed inductive types by iterated function types
- inductiveTyp
the indexed inductive types
- Definition Classes
- TermGeneratorNodes
- def indexedOtherHeadIsle(typF: Term)(typ: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
Extending an indexed introduction rule by a specific unrelated type
Extending an indexed introduction rule by a specific unrelated type
- typF
the indexed inductive type family
- typ
the type by which to extends
- returns
distribution on types
- Definition Classes
- TermGeneratorNodes
- def indexedOtherHeadNode(typF: Term): FlatMap[Typ[Term], Typ[Term]]
aggregating extending introduction types for indexed inductive types by unrelated types
aggregating extending introduction types for indexed inductive types by unrelated types
- typF
the indexed type family
- returns
distribution of terms
- Definition Classes
- TermGeneratorNodes
- def indexedSelfHeadNode(typF: Term): FlatMap[Typ[Term], Typ[Term]]
Aggregating extending indexed introduction rule by fully applied inductive type family.
Aggregating extending indexed introduction rule by fully applied inductive type family.
- typF
the type family
- returns
distribution on types.
- Definition Classes
- TermGeneratorNodes
- val inducFuncFoldedNode: GeneratorNode[Term]
Node for recursive definitions given an inductive definition, generating a domain and invoking the node getting codomain and recursion data
Node for recursive definitions given an inductive definition, generating a domain and invoking the node getting codomain and recursion data
- Definition Classes
- TermGeneratorNodes
- val inducFuncs: FlatMap[ExstInducStrucs, ExstFunc]
aggregated induction functions from inductive types
aggregated induction functions from inductive types
- Definition Classes
- TermGeneratorNodes
- def inducFuncsFolded(ind: ExstInducDefn): GeneratorNode[Term]
Inductive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data
Inductive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data
- Definition Classes
- TermGeneratorNodes
- def inducFuncsFoldedGivenDomNode(ind: ExstInducDefn, dom: Term): GeneratorNode[Term]
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in.
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in. Examples of domains are
Nat
,Vec(A)
andFin
- Definition Classes
- TermGeneratorNodes
- def inducFuncsForStruc(ind: ExstInducStrucs): ZipMapOpt[Typ[Term], Term, ExstFunc]
induction function for a specific structure, picking the type family
induction function for a specific structure, picking the type family
- ind
the inductive structure
- returns
distribution of functions
- Definition Classes
- TermGeneratorNodes
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def iterFuncIsle(targetTyp: Typ[Term])(typ: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
extending types of iterated functions targeting
W
by the typetyp
extending types of iterated functions targeting
W
by the typetyp
- targetTyp
the target type
- typ
the type by which it is extended
- returns
distribution of types
- Definition Classes
- TermGeneratorNodes
- def iterFuncNode(targetTyp: Typ[Term]): FlatMap[Typ[Term], Typ[Term]]
aggregating extensions of iterated function types
aggregating extensions of iterated function types
- targetTyp
target type
- returns
distribution of types
- Definition Classes
- TermGeneratorNodes
- def iterHeadNode(inductiveTyp: Typ[Term]): FlatMap[Typ[Term], Typ[Term]]
extension of the introduction rule for an inductive type
W
by a type of the form egA -> W
extension of the introduction rule for an inductive type
W
by a type of the form egA -> W
- inductiveTyp
the inductive type
W
- returns
distribution of types
- Definition Classes
- TermGeneratorNodes
- def iteratedApply(f: Term): GeneratorNode[Term]
node to generate partial applications of
f
from partial applications that are functions.node to generate partial applications of
f
from partial applications that are functions.- f
function to be applied
- returns
distribution of terms
- Definition Classes
- TermGeneratorNodes
- val lambdaForFuncWithDomFamily: BasePi[::[Typ[Term], HNil], ExstFunc]
nodes combining lambdas with given domain that are (dependent) function types, aggregated over all domains
nodes combining lambdas with given domain that are (dependent) function types, aggregated over all domains
- Definition Classes
- TermGeneratorNodes
- def lambdaIsle(typ: Typ[Term]): Island[Term, ParMapState, Term, Term]
An island to generate lambda terms, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.
An island to generate lambda terms, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.
- typ
the domain of the lambda
- Definition Classes
- TermGeneratorNodes
- def lambdaIsleForFuncWithDomain(dom: Typ[Term]): Island[ExstFunc, ParMapState, Term, Term]
lambda island for generating function with specified domain
lambda island for generating function with specified domain
- dom
the desired domain
- returns
distribution of functions
- Definition Classes
- TermGeneratorNodes
- val lambdaNode: FlatMap[Typ[Term], Term]
node combining lambda islands aggregated by type
node combining lambda islands aggregated by type
- Definition Classes
- TermGeneratorNodes
- def lambdaTypFamilyIsle(typ: Typ[Term]): GeneratorNode[ExstFunc]
An island to generate lambda terms that are type families, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.
An island to generate lambda terms that are type families, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in. Within the island types and type families are generated.
- typ
the domain of the lambda
- Definition Classes
- TermGeneratorNodes
- val lambdaTypFamilyNode: FlatMap[Typ[Term], ExstFunc]
node combining lambda islands targeting type families aggregated by type
node combining lambda islands targeting type families aggregated by type
- Definition Classes
- TermGeneratorNodes
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def nodeForTyp(typ: Typ[Term]): Option[GeneratorNode[Term]]
A node for targeting a (dependent function) type, with variable of the domain generated and the co-domain type (more generally fibre) targeted within the island.
A node for targeting a (dependent function) type, with variable of the domain generated and the co-domain type (more generally fibre) targeted within the island.
- typ
the target type
- returns
optional distribution.
- Definition Classes
- TermGeneratorNodes
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def otherHeadIsle(inductiveTyp: Typ[Term])(typ: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
extensions of the introduction rule types for an inductive type
W
by an unrelated typeC
; we may have a Pi-Type with domainC
rather than a FuncTyp there is no assumption on how the head typetyp
is generated, so this is reusable if only that is changed.extensions of the introduction rule types for an inductive type
W
by an unrelated typeC
; we may have a Pi-Type with domainC
rather than a FuncTyp there is no assumption on how the head typetyp
is generated, so this is reusable if only that is changed.- inductiveTyp
the inductive type
W
- typ
the type
C
by which we are extending the introduction rule type- returns
distribution of introduction rule types
- Definition Classes
- TermGeneratorNodes
- def otherHeadNode(inductiveTyp: Typ[Term]): FlatMap[Typ[Term], Typ[Term]]
aggregating extensions of inductive types by unrelated types
aggregating extensions of inductive types by unrelated types
- inductiveTyp
the inductive type being generated
- returns
distribution of introduction rule types.
- Definition Classes
- TermGeneratorNodes
- def partiallyApply(f: Term): Option[Map[Term, Term]]
single function application to generate partial applications of
f
, iff
is a functionsingle function application to generate partial applications of
f
, iff
is a function- f
the function to partially apply
- returns
distribution of terms
- Definition Classes
- TermGeneratorNodes
- def piIsle(typ: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
island to generate Pi-Types by taking variables with specified domain, similar to lambdaIsle
island to generate Pi-Types by taking variables with specified domain, similar to lambdaIsle
- typ
the domain for
- returns
distribution of types
- Definition Classes
- TermGeneratorNodes
- val piNode: FlatMap[Typ[Term], Typ[Term]]
aggregate generation of Pi-types from islands
aggregate generation of Pi-types from islands
- Definition Classes
- TermGeneratorNodes
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val recFuncFoldedNode: GeneratorNode[Term]
Node for recursive definitions picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data
Node for recursive definitions picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data
- Definition Classes
- TermGeneratorNodes
- val recFuncs: FlatMap[ExstInducStrucs, ExstFunc]
aggregate recursion functions from inductive types
aggregate recursion functions from inductive types
- Definition Classes
- TermGeneratorNodes
- def recFuncsFolded(ind: ExstInducDefn): GeneratorNode[Term]
Recursive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data
Recursive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data
- Definition Classes
- TermGeneratorNodes
- def recFuncsFoldedGivenDomNode(ind: ExstInducDefn, dom: Term): GeneratorNode[Term]
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in.
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in. Examples of domains are
Nat
,Vec(A)
andFin
- Definition Classes
- TermGeneratorNodes
- def selfHeadNode(inductiveTyp: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
extend an introduction rule type for an inductive type
W
byW -> ...
extend an introduction rule type for an inductive type
W
byW -> ...
- inductiveTyp
the inductive type being defined
- returns
distribution of types for introduction rules
- Definition Classes
- TermGeneratorNodes
- def sigmaIsle(typ: Typ[Term]): Island[Typ[Term], ParMapState, Typ[Term], Term]
island to generate Sigma-Types by taking variables with specified domain, similar to lambdaIsle
island to generate Sigma-Types by taking variables with specified domain, similar to lambdaIsle
- typ
the domain for
- returns
distribution of types
- Definition Classes
- TermGeneratorNodes
- val sigmaNode: FlatMap[Typ[Term], Typ[Term]]
aggregate generation of Sigma-types from islands
aggregate generation of Sigma-types from islands
- Definition Classes
- TermGeneratorNodes
- def simpleInductiveDefn(inductiveTyp: Typ[Term]): Map[Vector[Typ[Term]], ExstInducDefn]
builds an inductive definition, i.e.
builds an inductive definition, i.e. structure with type, from a bunch of introduction rules for a type
inductiveTyp
, we must separately specify how to build an introduction rules, as well as a vector of these.- inductiveTyp
the inductve type being defined
- returns
distribution on existential inductive structures
- Definition Classes
- TermGeneratorNodes
- def simpleInductiveStructure(inductiveTyp: Typ[Term]): Map[Vector[Typ[Term]], ExstInducStrucs]
builds an inductive structure from a bunch of introduction rules for a type
inductiveTyp
, we must separately specify how to build an introduction rules, as well as a vector of these.builds an inductive structure from a bunch of introduction rules for a type
inductiveTyp
, we must separately specify how to build an introduction rules, as well as a vector of these.- inductiveTyp
the inductve type being defined
- returns
distribution on existential inductive structures
- Definition Classes
- TermGeneratorNodes
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def targetInducBackNode(typ: Typ[Term]): MapOpt[ExstInducDefn, Term]
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here meant to be used for backward reasoning.
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here meant to be used for backward reasoning.
- Definition Classes
- TermGeneratorNodes
- def targetInducFuncsFolded(ind: ExstInducDefn, target: Typ[Term]): Option[GeneratorNode[Term]]
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data
- Definition Classes
- TermGeneratorNodes
- def targetInducNode(typ: Typ[Term]): FlatMapOpt[ExstInducDefn, Term]
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here
- Definition Classes
- TermGeneratorNodes
- val targetInducNodeFamily: BasePi[::[Typ[Term], HNil], Term]
Family of nodes for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here
Family of nodes for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here
- Definition Classes
- TermGeneratorNodes
- val termsByTyps: ZipFlatMap[Typ[Term], Term, Term]
terms generated by first choosing type and then term with the type; a form of backward reasoning
terms generated by first choosing type and then term with the type; a form of backward reasoning
- Definition Classes
- TermGeneratorNodes
- val tg: TermGenParams
- val typApplnBase: FiberProductMap[ExstFunc, Term, Typ[Term], Term]
function application to get terms by choosing a type family and then a term in its domain, but without conditioning
function application to get terms by choosing a type family and then a term in its domain, but without conditioning
- Definition Classes
- TermGeneratorNodes
- val typApplnNode: GeneratorNode[Typ[Term]]
function application to get types by choosing a type family and then a term in its domain, but without conditioning
function application to get types by choosing a type family and then a term in its domain, but without conditioning
- Definition Classes
- TermGeneratorNodes
- val typAsCodNodeFamily: BasePi[::[Typ[Term], HNil], Term]
Node for generating terms of a type (if possible) by multiple applications of functions targeting the type.
Node for generating terms of a type (if possible) by multiple applications of functions targeting the type.
- Definition Classes
- TermGeneratorNodes
- val typFamilyApplnNode: GeneratorNode[ExstFunc]
function application to get type families by choosing a type family and then a term in its domain, but without conditioning
function application to get type families by choosing a type family and then a term in its domain, but without conditioning
- Definition Classes
- TermGeneratorNodes
- val typFamilyUnifApplnNode: GeneratorNode[ExstFunc]
function application with unification starting with type families, with output conditioned to be a type family.
function application with unification starting with type families, with output conditioned to be a type family.
- Definition Classes
- TermGeneratorNodes
- val typFoldNode: FlatMap[ExstFunc, Typ[Term]]
Node family for fully folding type families to get types
Node family for fully folding type families to get types
- Definition Classes
- TermGeneratorNodes
- def typFromFamily(typF: Term): MapOpt[Term, Typ[Term]]
types from a type family by filtering partial applications to consider only types.
types from a type family by filtering partial applications to consider only types.
- typF
the type family
- returns
distribution of types.
- Definition Classes
- TermGeneratorNodes
- val typUnifApplnBase: ZipMapOpt[ExstFunc, Term, Term]
function application with unification starting with type families, but with output not conditioned.
function application with unification starting with type families, but with output not conditioned.
- Definition Classes
- TermGeneratorNodes
- val typUnifApplnNode: GeneratorNode[Typ[Term]]
function application with unification starting with type families, with output conditioned to be a type.
function application with unification starting with type families, with output conditioned to be a type.
- Definition Classes
- TermGeneratorNodes
- val unifApplnNode: ZipMapOpt[ExstFunc, Term, Term]
function application with unification node to get terms
function application with unification node to get terms
- Definition Classes
- TermGeneratorNodes
- 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])
- case object Appln extends (ExstFunc, Term) => Term with Product with Serializable
Wrapper for application to allow equality and
toString
to work.Wrapper for application to allow equality and
toString
to work.- Definition Classes
- TermGeneratorNodes
- case object CurryForTyp extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object FlipAppln extends (Term, ExstFunc) => Term with Product with Serializable
Wrapper for flipped application to allow equality and
toString
to work.Wrapper for flipped application to allow equality and
toString
to work.- Definition Classes
- TermGeneratorNodes
- case object FoldTypFamily extends (ExstFunc) => GeneratorNode[Typ[Term]] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object FoldedTargetFunctionNode extends (::[Typ[Term], HNil]) => FlatMapOpt[Term, Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object InducFuncsFolded extends (ExstInducDefn) => GeneratorNode[Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object LambdaIsle extends (Typ[Term]) => Island[Term, InitState, Term, Term] with Product with Serializable
Wrapper for lambda island to allow equality and
toString
to work.Wrapper for lambda island to allow equality and
toString
to work.- Definition Classes
- TermGeneratorNodes
- case object LambdaIsleForFuncWithDomain extends (::[Typ[Term], HNil]) => Island[ExstFunc, InitState, Term, Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object LambdaTypFamilyIsle extends (Typ[Term]) => GeneratorNode[ExstFunc] with Product with Serializable
Wrapper for lambda island tageting type families to allow equality and
toString
to work.Wrapper for lambda island tageting type families to allow equality and
toString
to work.- Definition Classes
- TermGeneratorNodes
- case object NodeForTyp extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object PiIsle extends (Typ[Term]) => Island[Typ[Term], InitState, Typ[Term], Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object RecFuncsFolded extends (ExstInducDefn) => GeneratorNode[Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object SigmaIsle extends (Typ[Term]) => Island[Typ[Term], InitState, Typ[Term], Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object TargetInducNode extends (::[Typ[Term], HNil]) => FlatMapOpt[ExstInducDefn, Term] with Product with Serializable
- Definition Classes
- TermGeneratorNodes
- case object UnifApplnOpt extends (ExstFunc, Term) => Option[Term] with Product with Serializable
Wrapper for unified application to allow equality and
toString
to work.Wrapper for unified application to allow equality and
toString
to work.- Definition Classes
- TermGeneratorNodes
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
- def →[B](y: B): (ParGenNodes, B)
- Implicit
- This member is added by an implicit conversion from ParGenNodes toArrowAssoc[ParGenNodes] performed by method ArrowAssoc in scala.Predef.
- Definition Classes
- ArrowAssoc
- Annotations
- @deprecated
- Deprecated
(Since version 2.13.0) Use
->
instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.