From 168217b2bd64d7eefd7ac4ada54cf80018309a11 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Jan 2024 18:36:52 -0800 Subject: [PATCH] chore: remove TODOs --- src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean | 3 +-- src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean | 3 +-- src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 3 +-- src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean | 3 +-- 4 files changed, 4 insertions(+), 8 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean index 1ca99f7d37..15368bed1f 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean @@ -63,8 +63,7 @@ builtin_simproc [simp, seval] reduceGT (( _ : Fin _) > _) := reduceBinPred ``G builtin_simproc [simp, seval] reduceGE (( _ : Fin _) ≥ _) := reduceBinPred ``GE.ge 4 (. ≥ .) /-- Return `.done` for Fin values. We don't want to unfold in the symbolic evaluator. -/ --- TODO: remove `simp` -builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do +builtin_simproc [seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue return .done { expr := e } diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean index e68ecebc39..376f7459e7 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean @@ -73,8 +73,7 @@ builtin_simproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do return .done { expr := toExpr v } /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/ --- TODO: remove `simp` -builtin_simproc [simp, seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do +builtin_simproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue return .done { expr := e } diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 95897687c4..5abb6efec8 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean @@ -55,8 +55,7 @@ builtin_simproc [simp, seval] reduceGT (( _ : Nat) > _) := reduceBinPred ``GT. builtin_simproc [simp, seval] reduceGE (( _ : Nat) ≥ _) := reduceBinPred ``GE.ge 4 (. ≥ .) /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/ --- TODO: remove `simp` -builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do +builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do unless (← getContext).unfoldGround do return .continue unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue return .done { expr := e } diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean index 3718e3db5f..8413696899 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean @@ -59,8 +59,7 @@ builtin_simproc [simp, seval] $(mkIdent `reduceGT):ident (( _ : $typeName) > _) builtin_simproc [simp, seval] $(mkIdent `reduceGE):ident (( _ : $typeName) ≥ _) := reduceBinPred ``GE.ge 4 (. ≥ .) /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/ --- TODO: remove `simp` -builtin_simproc [simp, seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do +builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do unless (← getContext).unfoldGround do return .continue unless (e.isAppOfArity ``OfNat.ofNat 3) do return .continue return .done { expr := e }