Packages

package proof

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. proof
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class ProofOps(prop: Boolean) extends Product with Serializable
    Annotations
    @library()
  2. case class RelReasoning[A](x: A, prop: Boolean) extends Product with Serializable

    Relational reasoning.

    Relational reasoning.

    { ((y :: ys) :+ x).last _ == _ | trivial | (y :: (ys :+ x)).last ==| trivial | (ys :+ x).last ==| snocLast(ys, x) | x }.qed

    Annotations
    @library()

Value Members

  1. implicit def any2RelReasoning[A](x: A): RelReasoning[A]
    Annotations
    @library()
  2. implicit def boolean2ProofOps(prop: Boolean): ProofOps
    Annotations
    @library() @inline()
  3. def by(proof: Boolean)(prop: Boolean): Boolean
    Annotations
    @library()
  4. def check(prop: Boolean): Boolean
    Annotations
    @library()
  5. def trivial: Boolean
    Annotations
    @library()
  6. object BoundedQuantifiers
    Annotations
    @library()
  7. object Internal

    Internal helper classes and methods for the 'proof' package.

Inherited from AnyRef

Inherited from Any

Ungrouped