From a9a3376443e4c6d9a5257bdd310966a59aa9e716 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jul 2023 14:00:48 +0200
Subject: Update a comment

---
 backends/lean/Base/Arith/Arith.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 2ff030fe..8bfad6ae 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -303,8 +303,7 @@ def scalarTacPreprocess (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
    add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
-   -- Reveal the concrete bounds - TODO: not too sure about that.
-   -- Maybe we should reveal the "concrete" bounds (after normalization)
+   -- Reveal the concrete bounds
    Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
                  ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
                  ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
-- 
cgit v1.2.3