Skip to content

Commit 65f8b27

Browse files
committed
Fix grind failure in Automata/NA/Sum.lean
1 parent 4a84152 commit 65f8b27

1 file changed

Lines changed: 3 additions & 1 deletion

File tree

Cslib/Computability/Automata/NA/Sum.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,9 @@ theorem iSum_language_eq {na : (i : I) → NA (State i) Symbol} {acc : (i : I)
7171
constructor
7272
· rintro ⟨ss, h_run, h_acc⟩
7373
simp only [mem_iUnion] at h_acc
74-
grind
74+
#adaptation_note
75+
/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
76+
grind [Accepts]
7577
· rintro ⟨i, ss_i, _⟩
7678
use ss_i.map (Sigma.mk i)
7779
simp only [mem_iUnion]

0 commit comments

Comments
 (0)