a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
11 lines
448 B
Text
11 lines
448 B
Text
inductive Palindrome : List α → Prop where
|
||
| nil : Palindrome []
|
||
| single : (a : α) → Palindrome [a]
|
||
| sandwish : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
|
||
|
||
theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse :=
|
||
match h with
|
||
| .nil => .nil
|
||
| .single a => Palindrome.single a
|
||
--^ textDocument/hover
|
||
| .sandwish a h => by simp; exact .sandwish _ (palindrome_reverse h)
|