From eb97bdb6761437e492bcf1a95b4fa43d2b69601b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 18:04:19 +0200
Subject: Improve progress to use assumptions and start working on a nice
 syntax

---
 backends/lean/Base/Diverge/Base.lean | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'backends/lean/Base/Diverge')

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
-- 
cgit v1.2.3