Value Members

1.  final def !=(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

2.  final def ##(): Int

   Definition Classes

   AnyRef → Any

3.  final def ==(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

4.  final def asInstanceOf[T0]: T0

   Definition Classes

   Any

5.  def clone(): AnyRef

   Attributes

   protected[lang]

   Definition Classes

   AnyRef

   Annotations

   @throws( ... ) @native()

6.  def elaborateDeclarations(context: Context, decls: List[InternalDeclaration], controller: Controller, logger: Option[(Constant) ⇒ Unit] = None)(implicit parentTerm: GlobalName): Elaboration

   Elaborates an derived declaration D using the inductive feature.

   Elaborates an derived declaration D using the inductive feature. This is used to reuse the functionality of this feature in different features, speciafically the reflection feature.

   context

   The context of D

   decls

   The internal declaration of the D

   parentTerm

   The path to D, used as prefix for the external declarations

7.  final def eq(arg0: AnyRef): Boolean

   Definition Classes

   AnyRef

8.  def equals(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

9.  def finalize(): Unit

   Attributes

   protected[lang]

   Definition Classes

   AnyRef

   Annotations

   @throws( classOf[java.lang.Throwable] )

10.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

11.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

12.  def inductionHypotheses(tpdecls: List[TypeLevel], tmdecls: List[TermLevel], context: Context)(implicit parent: GlobalName): (List[VarDecl], List[(GlobalName, (Term, Term) ⇒ Term)], List[(InternalDeclaration, VarDecl)], Context)

    Produces the proof predicate for each Type-Level and the corresponding induction hypothesis for each constructor

13.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

14.  def mapTerm(tm: Term, tp: Term, tpdecls: List[TypeLevel], predMap: List[(GlobalName, (Term, Term) ⇒ Term)], ctx: Context)(implicit parent: GlobalName): Option[Term]

    Tries to apply the correct predicate to the term tm of type tp

    Tries to apply the correct predicate to the term tm of type tp

    returns

    the predicate applied to this term, if a corresponding predicate is found, none otherwise

15.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

16.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

17.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

18.  def rBar(argCon: Context, tpdecls: List[TypeLevel], indProofDeclMap: List[(GlobalName, (Term, Term) ⇒ Term)])(implicit parent: GlobalName): Context
19.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

20.  def toString(): String

    Definition Classes

    AnyRef → Any

21.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

22.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

23.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()