Skip to content

Commit 72978be

Browse files
Update src/Std/Do/PredTrans.lean
Co-authored-by: Sebastian Graf <[email protected]>
1 parent f0f7ec2 commit 72978be

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Std/Do/PredTrans.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ Given a fixed postcondition, the *stronger* predicate transformer will yield a *
7878
precondition.
7979
-/
8080
def le (x y : PredTrans ps α) : Prop :=
81-
∀ Q, y.apply Q ⊢ₛ x.apply Q -- the weaker the precondition, the smaller the PredTrans
81+
∀ Q, y.apply Q ⊢ₛ x.apply Q
8282
instance : LE (PredTrans ps α) := ⟨le⟩
8383

8484
/--

0 commit comments

Comments
 (0)