summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge
diff options
context:
space:
mode:
authorSon Ho2023-07-12 18:04:19 +0200
committerSon Ho2023-07-12 18:04:19 +0200
commiteb97bdb6761437e492bcf1a95b4fa43d2b69601b (patch)
tree666cf4611365dea7d9d7240870e8acbcb8dc5a4d /backends/lean/Base/Diverge
parente010c10fb9a1e2d88b52a4f6b4a0865448276013 (diff)
Improve progress to use assumptions and start working on a nice syntax
Diffstat (limited to 'backends/lean/Base/Diverge')
-rw-r--r--backends/lean/Base/Diverge/Base.lean22
1 files changed, 0 insertions, 22 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index d2c91ff8..0a9ea4c4 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -6,28 +6,6 @@ import Mathlib.Tactic.Linarith
import Base.Primitives
-/-
-TODO:
-- we want an easier to use cases:
- - keeps in the goal an equation of the shape: `t = case`
- - if called on Prop terms, uses Classical.em
- 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: **casesm**
-- better split tactic
-- we need conversions to operate on the head of applications.
- Actually, something like this works:
- ```
- conv at Hl =>
- apply congr_fun
- simp [fix_fuel_P]
- ```
- Maybe we need a rpt ... ; focus?
-- simplifier/rewriter have a strange behavior sometimes
--/
-
-
/- TODO: this is very useful, but is there more? -/
set_option profiler true
set_option profiler.threshold 100