Skip to content

Commit

Permalink
simp only
Browse files Browse the repository at this point in the history
  • Loading branch information
awalterschulze committed Jan 10, 2025
1 parent 16788c8 commit 0eeef9c
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Katydid/Regex/SmartRegex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -332,11 +332,11 @@ private theorem orFromList_cons_NonEmptyList_is_or (x1: Regex α) (xs2: NonEmpty
| mk head tail =>
cases tail with
| nil =>
simp
simp only
unfold orFromList
rfl
| cons t1 t2 =>
simp
simp only
rw [orFromList_is_or_nonEmptyList]

theorem orToList_is_orFromList (x: Regex α):
Expand Down

0 comments on commit 0eeef9c

Please sign in to comment.