File tree Expand file tree Collapse file tree 1 file changed +5
-6
lines changed
Expand file tree Collapse file tree 1 file changed +5
-6
lines changed Original file line number Diff line number Diff line change @@ -71,19 +71,18 @@ def flatcat : (t : Tree a) → (xs: List a) → List a
7171def Tree.flatten₁ (t : Tree a) : List a :=
7272 flatcat t []
7373
74- theorem flatten_eq_helper_accum (t : Tree a) (xs: List a) :
75- t.flatten ++ xs = flatcat t xs := by
74+ theorem flatten_eq_helper_accum (t : Tree a) (xs: List a)
75+ : t.flatten ++ xs = flatcat t xs := by
7676 induction t generalizing xs with
7777 | null => rfl
7878 | node l x r ihl ihr =>
79- rw [flatcat, <- ihr]
80- rw [← ihl (x :: (r.flatten ++ xs))]
79+ rw [flatcat, ← ihr]
80+ rw [←ihl (x :: (r.flatten ++ xs))]
8181 rw [List.append_cons]
8282 rw [← List.append_assoc]
8383 rw [Tree.flatten]
8484
85- example (t: Tree a) :
86- t.flatten = t.flatten₁ := by
85+ example (t: Tree a) : t.flatten = t.flatten₁ := by
8786 induction t with
8887 | null => exact rfl
8988 | node l x r ihl ihr =>
You can’t perform that action at this time.
0 commit comments