Assertion

The Assertion class and Assertion.ofProp embedding.

class Std.Internal.Do.Assertion (α : Type w) extends Lean.Order.CompleteLattice α : Type w

An assertion type is equipped with a CompleteLattice structure, used as the carrier for pre- and postconditions.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• has_sup (c : α → Prop) : Exists (is_sup c)