Kim Morrison af03af5037 feat: simprocs for #[1,2,3,4,5][2] (#4765) ... None of these were working previously: ``` #check_simp #[1,2,3,4,5][2] ~> 3 #check_simp #[1,2,3,4,5][2]? ~> some 3 #check_simp #[1,2,3,4,5][7]? ~> none #check_simp #[][0]? ~> none #check_simp #[1,2,3,4,5][2]! ~> 3 #check_simp #[1,2,3,4,5][7]! ~> (default : Nat) #check_simp (#[] : Array Nat)[0]! ~> (default : Nat) ```		2024-07-17 03:05:17 +00:00
..
BuiltinSimprocs	feat: simprocs for #[1,2,3,4,5][2] (#4765)	2024-07-17 03:05:17 +00:00
Attr.lean	feat: use attribute command to add and erase simprocs (#3511)	2024-02-26 23:41:49 +00:00
BuiltinSimprocs.lean	feat: simprocs for #[1,2,3,4,5][2] (#4765)	2024-07-17 03:05:17 +00:00
Diagnostics.lean	feat: pretty print Array DiscrTree.Key (#4208)	2024-05-17 22:35:24 +00:00
Main.lean	chore: adjust List.replicate simp lemmas (#4687)	2024-07-08 15:29:19 +00:00
RegisterCommand.lean	chore: reorganising to reduce imports (#3790)	2024-03-27 11:15:01 +00:00
Rewrite.lean	fix: avoid unnecessary proof steps in simp (#4567)	2024-06-26 05:48:03 +00:00
SimpAll.lean	chore: missing registerTraceClass (#4369)	2024-06-06 00:53:16 +00:00
SimpCongrTheorems.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Simproc.lean	feat: use dsimprocs at dsimp	2024-03-05 14:42:05 -08:00
SimpTheorems.lean	chore: fix linter errors (#4502)	2024-06-19 18:24:08 +00:00
Types.lean	fix: remove PersistentHashMap.size	2024-06-19 20:21:34 +02:00