Packages

sealed trait IterFuncPtnMap[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F], TT <: Term with Subs[TT], DT <: Term with Subs[DT]] extends AnyRef

a family of the form P: A -> B -> W etc, or dependent versions of this as a function of W, together with the scala type of a codomain; has methods for defining induced functions and dependent functions.

O

scala type of terms of the type W

C

scala type of codomain

F

scala type of the family eg P: A -> W

TT

scala type of family type eg A -> B -> X, ie, codomain of induced function

DT

scala type of family type eg A -> B -> X, ie, codomain of induced function

Linear Supertypes
AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IterFuncPtnMap
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. type Cod = C
  2. type Family = F

    scala type (upper bound) for a member of the family, i.e., sections

Abstract Value Members

  1. abstract def apply(tp: Typ[O]): Typ[Family]

    returns the type corresponding to the pattern, such as A -> W, given the (inductive) type W, this is used mainly for constructor patterns, with the W being fixed.

  2. abstract def depTarget(xs: Func[O, Typ[Cod]]): (Family) => Typ[DT]

    dependent target scala type.

  3. abstract def induced(f: Func[O, Cod]): (Family) => TT

    function induced by f: W -> X of type (A -> W) -> (A -> X) etc

    function induced by f: W -> X of type (A -> W) -> (A -> X) etc

    f

    function from which to induce

  4. abstract def inducedDep(f: FuncLike[O, Cod]): (Family) => DT

    dependent function induced by dependent f: W -> X(s) of type (A -> W) -> ((a : A) ~> Xs(a)) etc

    dependent function induced by dependent f: W -> X(s) of type (A -> W) -> ((a : A) ~> Xs(a)) etc

    f

    dependent function from which to induce

  5. abstract def subs(x: Term, y: Term): IterFuncPtnMap[O, C, F, TT, DT]
  6. abstract def target(x: Typ[Cod]): Typ[TT]

    target scala type.

  7. abstract val univLevel: Int

    the universe containing the type