diff options
| author | Son Ho | 2023-07-12 14:34:55 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-12 14:34:55 +0200 |
| commit | a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 (patch) | |
| tree | b8bc72479804fcd416fea42478d7e7945845cbe7 /backends/lean/Base/Diverge/Base.lean | |
| parent | 6166c410a4b3353377e640acbae9f56e877a9118 (diff) | |
Finish a first version of the progress tactic
Diffstat (limited to 'backends/lean/Base/Diverge/Base.lean')
| -rw-r--r-- | backends/lean/Base/Diverge/Base.lean | 2 |
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: |