Skip to content

Commit 1b9b700

Browse files
committed
Update to lean v4.29.0
1 parent 599e4e0 commit 1b9b700

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

Effects/Prog.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,13 +165,15 @@ instance {effs : List Effect} : Monad (Prog effs) where
165165
pure := Prog.var
166166
bind := Prog.bind
167167

168+
@[reducible]
168169
def opsMem
169170
{effs : List Effect}
170171
{e : Effect} :
171172
e ∈ effs → e.ops ∈ List.map Effect.ops effs
172173
| .here => .here
173174
| .there m => .there (opsMem m)
174175

176+
@[reducible]
175177
def scpsMem
176178
{effs : List Effect}
177179
{e : Effect} :

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.28.0
1+
leanprover/lean4:v4.29.0

0 commit comments

Comments
 (0)