Skip to content

Commit 69db505

Browse files
committed
Bump toolchain
1 parent 800847d commit 69db505

2 files changed

Lines changed: 3 additions & 3 deletions

File tree

Valaig/Aig/Iter.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ private theorem IsPlausibleStep_iff {step} :
6565
step = .yield ⟨⟨inc itm.internalState.idx⟩⟩ itm.internalState.idx
6666
else
6767
step = .done := by
68-
simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep]
68+
simp only [Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIterator]
6969
grind only [Iter, Std.IterM]
7070

7171
@[local simp, local grind =]
@@ -75,7 +75,7 @@ private theorem IsPlausibleStep_iff' {step} :
7575
step = .yield ⟨⟨inc it.internalState.idx⟩⟩ it.internalState.idx
7676
else
7777
step = .done := by
78-
simp only [Std.Iter.IsPlausibleStep, Std.IterStep.mapIterator, Std.Iter.toIterM, Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep]
78+
simp only [Std.Iter.IsPlausibleStep, Std.IterStep.mapIterator, Std.Iter.toIterM, Std.IterM.IsPlausibleStep, Std.Iterator.IsPlausibleStep, instIterator]
7979
grind only [Iter, Std.Iter]
8080

8181
@[local simp, local grind =]

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2026-02-11
1+
leanprover/lean4:nightly-2026-03-05

0 commit comments

Comments
 (0)