max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup after renaming get_elem_tactic_trivial

Browse source
This commit is contained in:
Kim Morrison 2025-05-26 10:28:22 +10:00
parent a5567618ac
commit 50474fef78
5 changed files with 2 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Data/Range/Basic.lean
View file

@ -86,6 +86,3 @@ theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r)
macro_rules
| `(tactic| get_elem_tactic_extensible) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)
macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)

3
src/Init/GetElem.lean
View file

@ -283,9 +283,6 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
macro_rules
| `(tactic| get_elem_tactic_extensible) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_extensible; done)
macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| (with_reducible apply Fin.val_lt_of_le); get_elem_tactic_trivial; done)
end Fin
namespace List

4
src/Init/Tactics.lean
View file

@ -1933,9 +1933,7 @@ syntax "get_elem_tactic_trivial" : tactic
macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| omega)
macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| simp +arith; done)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| omega)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp +arith; done)
macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| trivial)
/--
`get_elem_tactic` is the tactic automatically called by the notation `arr[i]`

3
src/Lean/Elab/Tactic.lean
View file

@ -51,6 +51,3 @@ import Lean.Elab.Tactic.TreeTacAttr
import Lean.Elab.Tactic.ExposeNames
import Lean.Elab.Tactic.SimpArith
import Lean.Elab.Tactic.Lets
elab "get_elem_tactic_trivial" : tactic => do
throwError "`get_elem_tactic_trivial` has been renamed to `get_elem_tactic_extensible`"

2
tests/lean/run/grind_indexmap.lean
View file

@ -6,7 +6,7 @@ import Std.Data.HashMap
set_option grind.warning false
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| grind)
macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
open Std