Kyle Miller 62521f4f2d fix: let congr conv tactic handle "over-applied" functions (#5861) ... Adds ability to chain congruence lemmas when a function's arity is less than the number of supplied arguments. This improves `congr` as well as all conv tactics implemented using `congr`, like `arg` and `enter`. (The non-conv `congr` tactic still needs to be fixed.) Toward #2942.		2024-10-28 07:34:33 +00:00
..
bench	test: big_omega benchmark (#5817)	2024-10-24 07:26:29 +00:00
compiler	doc: update documentation and tests for toUIntX functions (#5497)	2024-09-29 08:11:04 +00:00
elabissues
ir
lean	fix: let congr conv tactic handle "over-applied" functions (#5861)	2024-10-28 07:34:33 +00:00
pkg	test: check that recusive functions do not apply attriubutes twices (#5480)	2024-09-26 10:30:37 +00:00
playground	feat: rename Array.shrink to take, and relate to List.take (#5796)	2024-10-21 23:35:32 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain