Skip to content

Commit 0743e78

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

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Std/Do/SPred/SPred.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ theorem ext_cons {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funex
4646

4747
/--
4848
A pure proposition `P : Prop` embedded into `SPred`.
49-
Prefer to use idiom bracket notation `⌜P⌝`.
49+
Prefer to use notation `⌜P⌝`.
5050
-/
5151
def pure {σs : List (Type u)} (P : Prop) : SPred σs := match σs with
5252
| [] => ULift.up P

0 commit comments

Comments
 (0)