package proof
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- proof
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Type Members
-
case class
ProofOps(prop: Boolean) extends Product with Serializable
- Annotations
- @library()
-
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
-
implicit
def
any2RelReasoning[A](x: A): RelReasoning[A]
- Annotations
- @library()
-
implicit
def
boolean2ProofOps(prop: Boolean): ProofOps
- Annotations
- @library() @inline()
-
def
by(proof: Boolean)(prop: Boolean): Boolean
- Annotations
- @library()
-
def
check(prop: Boolean): Boolean
- Annotations
- @library()
-
def
trivial: Boolean
- Annotations
- @library()
-
object
BoundedQuantifiers
- Annotations
- @library()
-
object
Internal
Internal helper classes and methods for the 'proof' package.