Packages

c

provingground.learning

CompositeProver

class CompositeProver[D] extends AnyRef

Linear Supertypes
AnyRef, Any
Known Subclasses
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. CompositeProver
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new CompositeProver()(implicit arg0: Monoid[D])

Type Members

  1. case class AnyOf(provers: Vector[Prover], parallel: Boolean) extends Prover with Product with Serializable
  2. case class BothOf(first: Prover, second: Prover, zipProofs: (Term, Term) => Option[Term]) extends Prover with Product with Serializable
  3. case class Contradicted(prover: Prover, data: D) extends Result with Product with Serializable
  4. case class Elementary(lp: LocalProverStep, getData: (LocalProverStep) => Task[D], isSuccess: (D) => Task[Boolean]) extends Prover with Product with Serializable
  5. case class MapProof(prover: Prover, proofMap: (Term) => Option[Term]) extends Prover with Product with Serializable
  6. case class OneOf(first: Prover, second: Prover) extends Prover with Product with Serializable
  7. case class Proved(prover: Prover, data: D) extends Result with Product with Serializable
  8. sealed trait Prover extends AnyRef
  9. sealed trait Result extends AnyRef
  10. case class SomeOf(provers: Vector[Prover]) extends Prover with Product with Serializable
  11. case class Unknown(data: D, partials: Set[Result]) extends Result with Product with Serializable
  12. case class Xor(hyp: Prover, contra: Prover) extends Prover with Product with Serializable

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def +(other: String): String
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toany2stringadd[CompositeProver[D]] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ->[B](y: B): (CompositeProver[D], B)
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toArrowAssoc[CompositeProver[D]] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  8. def combineResults(x: Result, y: Result): Product with Result with Serializable { def flip: Product with CompositeProver.this.Result with java.io.Serializable }
  9. def consequences(result: Result): Set[Result]
  10. def contradictedProvers(results: Set[Result]): Set[Prover]
  11. val empty: D
  12. def ensuring(cond: (CompositeProver[D]) => Boolean, msg: => Any): CompositeProver[D]
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toEnsuring[CompositeProver[D]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  13. def ensuring(cond: (CompositeProver[D]) => Boolean): CompositeProver[D]
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toEnsuring[CompositeProver[D]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  14. def ensuring(cond: Boolean, msg: => Any): CompositeProver[D]
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toEnsuring[CompositeProver[D]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  15. def ensuring(cond: Boolean): CompositeProver[D]
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toEnsuring[CompositeProver[D]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  16. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  18. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toStringFormat[CompositeProver[D]] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @inline()
  19. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  20. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  21. def isContradicted(results: Set[Result], prover: Prover): Boolean
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. def isProved(results: Set[Result], prover: Prover): Boolean
  24. def mergeResults(res: Iterable[Result]): Result
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  28. def proveSome(provers: Vector[Prover], results: Vector[Result], data: D, useData: (D) => (LocalProverStep) => LocalProverStep): Task[(Vector[Result], D)]
  29. def provedProvers(results: Set[Result]): Set[Prover]
  30. def purge(results: Set[Result], prover: Prover): Option[Prover]

    Purge components of the result that have been contradicted.

  31. def sequenceResult(provers: Vector[Prover], accum: D, partials: Set[Result]): Task[Result]
  32. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  33. def toString(): String
    Definition Classes
    AnyRef → Any
  34. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  35. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  36. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated
  2. def [B](y: B): (CompositeProver[D], B)
    Implicit
    This member is added by an implicit conversion from CompositeProver[D] toArrowAssoc[CompositeProver[D]] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @deprecated
    Deprecated

    (Since version 2.13.0) Use -> instead. If you still wish to display it as one character, consider using a font with programming ligatures such as Fira Code.

Inherited from AnyRef

Inherited from Any

Inherited by implicit conversion any2stringadd fromCompositeProver[D] to any2stringadd[CompositeProver[D]]

Inherited by implicit conversion StringFormat fromCompositeProver[D] to StringFormat[CompositeProver[D]]

Inherited by implicit conversion Ensuring fromCompositeProver[D] to Ensuring[CompositeProver[D]]

Inherited by implicit conversion ArrowAssoc fromCompositeProver[D] to ArrowAssoc[CompositeProver[D]]

Ungrouped