Skip to content

Commit 5aae34e

Browse files
committed
Fix variable naming of isRestrictedPath_iff_isPath
1 parent d153f47 commit 5aae34e

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

TraceTheory/TraceTheory/Computability.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -756,7 +756,7 @@ theorem isRestrictedPath_iff_isPath {i j : Fin n} {x : List α} :
756756
simp only [matches'_foldl_sum] at h_match
757757
simp only [Language.mem_add] at h_match
758758
sorry
759-
| trans k i' j' x₁ x₂ h₁ hlt h₂ ih₁ ih₂ =>
759+
| trans i' j' m x₁ x₂ h₁ hlt h₂ ih₁ ih₂ =>
760760
sorry
761761
· sorry
762762

0 commit comments

Comments
 (0)