1 parent a874b47 commit dd3418eCopy full SHA for dd3418e
1 file changed
correctness/RegexCorrectness/VM/CharStep/Lemmas.lean
@@ -37,7 +37,7 @@ theorem eq_updates_of_mem_next {i k} (h : stepChar (HistoryStrategy s) nfa wf po
37
next'.updates[k] = next.updates[k] := by
38
simp only [HistoryStrategy.update_def, stepChar, Fin.getElem_fin] at h
39
split at h
40
- · · expose_names; exact εClosure.eq_updates_of_mem_next h mem
+ · expose_names; exact εClosure.eq_updates_of_mem_next h mem
41
· grind only
42
43
0 commit comments