lean2/tests/lean/change_tac_fail.lean
Leonardo de Moura 368f9d347e refactor(frontends/lean): approach used to parse tactics
The previous approach was too fragile

TODO: we should add separate parsing tables for tactics
2015-03-05 18:11:21 -08:00

12 lines
288 B
Text

import data.list
open list
variable {T : Type}
theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
| append.assoc nil t u := by esimp
| append.assoc (a :: l) t u :=
begin
change (a :: (l ++ t ++ u) = (a :: l) ++ (t ++ a)),
rewrite append.assoc
end