Packages

object InductiveDefinition

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

Type Members

  1. case class DataCons[H <: Term with Subs[H], C <: Term with Subs[C], D <: Term with Subs[D]](data: D, cons: Term, defn: (D) => (FuncLike[H, C]) => (H) => Option[C], tail: InductiveDefinition[H, C], replacement: (Term) => (Term) => (Func[H, Typ[C]]) => Option[DataCons[H, C, D]] = (_: Term) => (_: Term) => (_: Func[H, Typ[C]]) => None) extends InductiveDefinition[H, C] with Product with Serializable

    an additional case for an InductiveDefinition, depending on definition data data

  2. case class Empty[H <: Term with Subs[H], C <: Term with Subs[C]](fibre: Func[H, Typ[C]]) extends InductiveDefinition[H, C] with Product with Serializable

    empty InductiveDefinition, always a formal application.