max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta/Tactic/Simp
History
Leonardo de Moura a23292f049
feat: add option tactic.skipAssignedInstances := true for backward compatibilty (#3526) 
When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match the
assigned one the rewrite is not performed. This option has been added
for backward compatibility.
2024-02-28 05:52:29 +00:00
..
BuiltinSimprocs refactor: use LitValue.lean to implement simprocs 2024-02-24 16:08:07 -08: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 BitVec (#3407) 2024-02-19 14:01:00 -08:00
Main.lean feat: add option tactic.skipAssignedInstances := true for backward compatibilty (#3526) 2024-02-28 05:52:29 +00:00
RegisterCommand.lean feat: use attribute command to add and erase simprocs (#3511) 2024-02-26 23:41:49 +00:00
Rewrite.lean feat: add option tactic.skipAssignedInstances := true for backward compatibilty (#3526) 2024-02-28 05:52:29 +00:00
SimpAll.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SimpCongrTheorems.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Simproc.lean feat: add option tactic.skipAssignedInstances := true for backward compatibilty (#3526) 2024-02-28 05:52:29 +00:00
SimpTheorems.lean feat: use attribute command to add and erase simprocs (#3511) 2024-02-26 23:41:49 +00:00
Types.lean feat: use attribute command to add and erase simprocs (#3511) 2024-02-26 23:41:49 +00:00