summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge
diff options
context:
space:
mode:
authorSon Ho2023-07-12 14:34:55 +0200
committerSon Ho2023-07-12 14:34:55 +0200
commita18d899a2c2b9bdd36f4a5a4b70472c12a835a96 (patch)
treeb8bc72479804fcd416fea42478d7e7945845cbe7 /backends/lean/Base/Diverge
parent6166c410a4b3353377e640acbae9f56e877a9118 (diff)
Finish a first version of the progress tactic
Diffstat (limited to 'backends/lean/Base/Diverge')
-rw-r--r--backends/lean/Base/Diverge/Base.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index e22eb914..d2c91ff8 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -14,7 +14,7 @@ TODO:
Actually, the cases from mathlib seems already quite powerful
(https://leanprover-community.github.io/mathlib_docs/tactics.html#cases)
For instance: cases h : e
- Also: cases_matching
+ Also: **casesm**
- better split tactic
- we need conversions to operate on the head of applications.
Actually, something like this works: