Skip to content

Commit 0eeef9c

Browse files
simp only
1 parent 16788c8 commit 0eeef9c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Katydid/Regex/SmartRegex.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -332,11 +332,11 @@ private theorem orFromList_cons_NonEmptyList_is_or (x1: Regex α) (xs2: NonEmpty
332332
| mk head tail =>
333333
cases tail with
334334
| nil =>
335-
simp
335+
simp only
336336
unfold orFromList
337337
rfl
338338
| cons t1 t2 =>
339-
simp
339+
simp only
340340
rw [orFromList_is_or_nonEmptyList]
341341

342342
theorem orToList_is_orFromList (x: Regex α):

0 commit comments

Comments
 (0)