Packages

object ExstInducStrucs

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

Type Members

  1. case class ConsSeqExst[SS <: HList, H <: Term with Subs[H], Intros <: HList](cs: ConstructorSeqTL[SS, H, Intros], intros: Vector[Term]) extends ExstInducStrucs with Product with Serializable
  2. case class IndConsSeqExst[SS <: HList, H <: Term with Subs[H], F <: Term with Subs[F], Index <: HList, Intros <: HList](cs: IndexedConstructorSeqDom[SS, H, F, Index, Intros], intros: Vector[Term])(implicit evidence$1: TermList[Index]) extends ExstInducStrucs with Product with Serializable
  3. case class LambdaInduc(variable: Term, struct: ExstInducStrucs) extends ExstInducStrucs with Product with Serializable
  4. case class OrElse(first: ExstInducStrucs, second: ExstInducStrucs) extends ExstInducStrucs with Product with Serializable

Value Members

  1. def get(typ: Term, intros: Vector[Term]): ExstInducStrucs
  2. def getIndexed(typF: Term, intros: Vector[Term]): ExstInducStrucs
  3. def goalDomainFmly(ind: ExstInducStrucs, fmly: Term, target: Typ[Term]): Option[(Term, Term)]

    Helper for generating domains targeting a specifed type for a given inductive structure, with an inductive definition also given.

    Helper for generating domains targeting a specifed type for a given inductive structure, with an inductive definition also given. Examples of domains are Nat, Vec(A) and Fin.

  4. case object Base extends ExstInducStrucs with Product with Serializable
  5. case object SimpleBase extends ExstInducStrucs with Product with Serializable