lean4-htt/tests
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
..
bench chore: speedcenter: count max symbols in shared libraries (#3418) 2024-02-20 19:25:24 +00:00
compiler fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
elabissues feat: add bitwise operations to reduceNat? and kernel (#3134) 2024-01-11 18:12:45 +00:00
ir feat: lake: GNU/BSD OS detection in test scripts (#3180) 2024-01-14 02:49:38 +00:00
lean feat: add option tactic.skipAssignedInstances := true for backward compatibilty (#3526) 2024-02-28 05:52:29 +00:00
pkg feat: simproc sets 2024-02-01 16:58:54 +11:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain