abstract class MacroInference extends BranchInference

An inference encapsulating multiple inferences, to be expanded on demand.

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

Instance Constructors

  1. new MacroInference(_providedFormulas: Set[CertFormula], _boundConstants: Set[ConstantTerm])

Abstract Value Members

  1. abstract def expand: Iterator[BranchInference]

    The represented inferences.

Concrete Value Members

  1. val assumedFormulas: Set[CertFormula]
    Definition Classes
    MacroInference → BranchInference
  2. lazy val constants: Set[ConstantTerm]

    Set of constants occurring in this inference.

    Set of constants occurring in this inference.

    Definition Classes
    BranchInference
  3. val localBoundConstants: Set[ConstantTerm]
    Definition Classes
    MacroInference → BranchInference
  4. def propagateConstraint(closingConstraint: Conjunction): Nothing

    Define the modification imposed by this rule application on the closing constraint.

    Define the modification imposed by this rule application on the closing constraint.

    Definition Classes
    MacroInference → BranchInference
  5. val providedFormulas: Set[CertFormula]

    Formulae that are introduced into the antecedent by this rule application.

    Formulae that are introduced into the antecedent by this rule application. This will implicitly simplify formulae (all simplifications that are built into the datastructures are carried out).

    Definition Classes
    MacroInference → BranchInference
  6. def toString(): String
    Definition Classes
    MacroInference → AnyRef → Any