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.  val Bool: OMID
5.  def Cong(pr: VarDecl, func: VarDecl): Term
6.  def Cong(prTp: Term, prDf: Term, funcTp: Term, funcDf: Term): Term

   More convenient version of CONG, which manually infers the first four arguments

7.  def CongAppl(prTp: Term, prDf: Term, tm: Term): (Term, Term)

   Takes a predicate pr: ⊦ x ≐ y for x: C → D, y: C → D and a term tm: C and returns a predicate ⊦ f x ≐ f y, where f x := x tm

   Takes a predicate pr: ⊦ x ≐ y for x: C → D, y: C → D and a term tm: C and returns a predicate ⊦ f x ≐ f y, where f x := x tm

   tm

   the term tm: C

   returns

   the type and and proof of the resulting predicate

8.  def Congs(prInitialTp: Term, prInitialDf: Term, argCtx: Context): (Term, Term)

   Folds a chain of Congs over a list of arguments, given the initial predicate prInitial and the type of the initial terms

   Folds a chain of Congs over a list of arguments, given the initial predicate prInitial and the type of the initial terms

   prInitialTp

   the type of the initial predicate : ⊦ x ≐ y

   prInitialDf

   the proof of the initial predicate : ⊦ x ≐ y

   argCtx

   the chain of arguments to which the terms are to be applied

   returns

   the type and and proof of the resulting predicate

9.  val Contra: OMID
10.  val False: OMID
11.  val Prop: Term
12.  val True: OMID
13.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

14.  def clone(): AnyRef

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()

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

    Definition Classes

    AnyRef

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

    Definition Classes

    AnyRef → Any

17.  def finalize(): Unit

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

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

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

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

19.  def getConstants(decls: List[Declaration], con: Controller): List[Constant]

    parse the declarations into constants, flattening PlainIncludes

    parse the declarations into constants, flattening PlainIncludes

    decls

    the declarations to parse

    con

    the controller

20.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

21.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

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

    Definition Classes

    AnyRef

23.  def neg(tp: Term): Term

    negate the statement in the type

24.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

25.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

26.  def parseInternalDeclarations(dd: DerivedDeclaration, con: Controller, ctx: Option[Context] = None, isConstructor: Option[(Constant) ⇒ (Boolean, Option[GlobalName])] = None): List[InternalDeclaration]

    Parse the internal declarations of dd

    Parse the internal declarations of dd

    dd

    the derived declaration whoose internal declarations to parse

    con

    the controller

    ctx

    (optional) a context to parse the declarations in

    isConstructor

    (optional) computes whether the declaration is a constructor and if so its typelevel Needs to be given for constructors over defined typelevels

27.  def parseInternalDeclarationsIntoConstants(dd: DerivedDeclaration, con: Controller): List[Constant]

    Reads the internal declarations (assumed to be constants) of a derivedDeclaration unfolding PlainIncludes

    Reads the internal declarations (assumed to be constants) of a derivedDeclaration unfolding PlainIncludes

    dd

    the derived declaration whoose internal declaration to read

    con

    the controller

28.  def parseInternalDeclarationsSubstitutingDefiniens(dd: DerivedDeclaration, con: Controller, ctx: Option[Context] = None, isConstructor: Option[(Constant) ⇒ (Boolean, Option[GlobalName])] = None): List[InternalDeclaration]

    Reads in the internal declarations of the given derived declaration and parses them into internal declarations.

    Reads in the internal declarations of the given derived declaration and parses them into internal declarations. It also will expand any references to previous declarations in terms of their definiens, if existent

    dd

    the derived declaration whoose declarations to parse

    con

    the controller, needed to parse the delarations

    ctx

    (optional) the (outer) context of the declarations

    isConstructor

    (optional) computes whether the declaration is a constructor and if so its typelevel Needs to be given for constructors over defined typelevels

29.  def readInternalDeclarations(consts: List[Constant], con: Controller, ctx: Option[Context] = None, isConstructor: Option[(Constant) ⇒ (Boolean, Option[GlobalName])] = None)(implicit parent: GlobalName): List[InternalDeclaration]
30.  def readInternalDeclarationsSubstitutingDefiniens(decls: List[Constant], con: Controller, ctx: Option[Context] = None, isConstructor: Option[(Constant) ⇒ (Boolean, Option[GlobalName])] = None)(implicit parent: GlobalName): List[InternalDeclaration]

    Reads in the given constants and parses them into Internal declarations.

    Reads in the given constants and parses them into Internal declarations. It also will expand any references to previous declarations in terms of their definiens, if existent

    decls

    the declarations to parse

    con

    the controller, needed to parse the delarations

    ctx

    (optional) the (outer) context of the declarations

    isConstructor

    (optional) computes whether the declaration is a constructor and if so its typelevel Needs to be given for constructors over defined typelevels

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

    Definition Classes

    AnyRef

32.  val theory: MPath
33.  val theoryPath: MPath
34.  def toString(): String

    Definition Classes

    AnyRef → Any

35.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()

38.  object CONG

    To allow for more user friendly inductive-proof declarations Takes a predicate pr: ⊦ x ≐ y for x: A, y: A, a (initial) function f: A → B and returns a predicate ⊦ f a ≐ f b

39.  object Ded
40.  object Eq
41.  object MAP
42.  object NONE
43.  object Neq
44.  object OPTION
45.  object SOME