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.  def applyInstanciated(arg: Term, params: List[Term])(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

5.  def applyInstanciated(args: Context, params: List[Term])(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

6.  def applyInstanciated(args: List[Term], params: List[Term])(implicit parent: GlobalName): Term

   apply the internal declaration to the given argument context and with its context instanciated to the given parameters

   apply the internal declaration to the given argument context and with its context instanciated to the given parameters

   args

   the arguments to apply the internal declaration to

   params

   the parameters to instanciate the context to

   parent

   (implicit) the path of the parent derived declaration

   Definition Classes

   InternalDeclaration

7.  def applyTo(tm: Term)(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

8.  def applyTo(args: Context)(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

9.  def applyTo(args: List[Term])(implicit parent: GlobalName): Term

   apply the internal declaration to the given argument context

   apply the internal declaration to the given argument context

   Definition Classes

   InternalDeclaration

10.  def argContext(suffix: Option[String] = None)(implicit parent: GlobalName): (Context, Term)

    Build a context quantifying over all arguments and the term of this constructor applied to those arguments

    Build a context quantifying over all arguments and the term of this constructor applied to those arguments

    suffix

    (optional) a suffix to append to the local name of each independent variable declaration in the returned context

    Definition Classes

    InternalDeclaration

11.  val args: List[(Option[LocalName], Term)]

    Definition Classes

    TermLevel → InternalDeclaration

12.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

13.  def clone(): AnyRef

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()

14.  def context: Context

    Definition Classes

    InternalDeclaration

15.  val ctx: Option[Context]

    Definition Classes

    TermLevel → InternalDeclaration

16.  val df: Option[Term]

    Definition Classes

    TermLevel → InternalDeclaration

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

    Definition Classes

    AnyRef

18.  def externalDf(implicit parent: GlobalName): Option[Term]

    like df but with all names externalized

    like df but with all names externalized

    Definition Classes

    InternalDeclaration

19.  def externalPath(implicit parent: GlobalName): GlobalName

    like path but with externalized path

    like path but with externalized path

    Definition Classes

    InternalDeclaration

20.  def externalRet(implicit parent: GlobalName): Term

    Definition Classes

    InternalDeclaration

21.  def externalTp(implicit parent: GlobalName): Term

    like tp but with all names externalized

    like tp but with all names externalized

    Definition Classes

    InternalDeclaration

22.  def finalize(): Unit

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

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

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

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

24.  def getTpl: TypeLevel
25.  def getTplArgs: List[Term]
26.  def injDecls(simplifyTag: Boolean = false)(implicit parent: GlobalName): List[Constant]

    Generate injectivity declaration for the term constructor d

    Generate injectivity declaration for the term constructor d

    parent

    the parent declared module of the derived declaration to elaborate

    Definition Classes

    TermLevel

27.  def internalTp: Term

    Definition Classes

    InternalDeclaration

28.  def isConstructor: Boolean

    Check whether the TermLevel is a constructor or outgoing

    Check whether the TermLevel is a constructor or outgoing

    Definition Classes

    Constructor → TermLevel → InternalDeclaration

29.  def isIndependentArgument(arg: (Option[LocalName], Term)): Boolean

    checks whether the type of the declaration is dependent on the given argument

    checks whether the type of the declaration is dependent on the given argument

    Definition Classes

    InternalDeclaration

30.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

31.  def isOutgoing: Boolean

    Definition Classes

    InternalDeclaration

32.  def isSimplyTyped(): Boolean

    checks whether the declaration is simply typed

    checks whether the declaration is simply typed

    Definition Classes

    InternalDeclaration

33.  def isTypeLevel: Boolean

    Definition Classes

    TermLevel → InternalDeclaration

34.  def makeVar(name: String): VarDecl

    a var decl with a fresh name of the same type as this one

    a var decl with a fresh name of the same type as this one

    Definition Classes

    TermLevel

35.  def name: LocalName

    Definition Classes

    InternalDeclaration

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

    Definition Classes

    AnyRef

37.  val notC: Option[NotationContainer]

    Definition Classes

    TermLevel

38.  def notation: NotationContainer

    Definition Classes

    TermLevel → InternalDeclaration

39.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

40.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

41.  val path: GlobalName

    Definition Classes

    TermLevel → InternalDeclaration

42.  val ret: Term

    Definition Classes

    TermLevel → InternalDeclaration

43.  def surjDecl(simplifyTag: Boolean = false)(implicit parent: GlobalName): Constant

    Generate surjectivity declaration for the term constructor d

    Generate surjectivity declaration for the term constructor d

    parent

    the parent declared module of the derived declaration to elaborate

    Definition Classes

    TermLevel

44.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

45.  def tm: Option[Term]

    Definition Classes

    TermLevel

46.  def toConstant(implicit parent: GlobalName): Constant

    Definition Classes

    InternalDeclaration

47.  def toConstant(simplifyTag: Boolean)(implicit parent: GlobalName): Constant

    Definition Classes

    InternalDeclaration

48.  def toString(): String

    Definition Classes

    InternalDeclaration → AnyRef → Any

49.  def toString(termPresenter: Option[(Term) ⇒ String]): String

    Definition Classes

    InternalDeclaration

50.  def toTerm(implicit parent: GlobalName): Term

    apply the internal declaration to its context

    apply the internal declaration to its context

    parent

    (implicit) the path of the parent derived declaration

    Definition Classes

    InternalDeclaration

51.  def toTermInstanciated(params: List[Term])(implicit parent: GlobalName): Term

    apply the internal declaration to a list of parameters instanciating its context

    apply the internal declaration to a list of parameters instanciating its context

    params

    the parameters to instanciate the context to

    parent

    (implicit) the path of the parent derived declaration

    Definition Classes

    InternalDeclaration

52.  def toVarDecl: VarDecl

    Definition Classes

    InternalDeclaration

53.  def tp: Term

    Definition Classes

    InternalDeclaration

54.  def translate(tr: Translator): InternalDeclaration

    applies a term translator to the arguments and definien of an internal declaration

    applies a term translator to the arguments and definien of an internal declaration

    tr

    the translator to apply

    Definition Classes

    InternalDeclaration

55.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()