lean4-htt/tests
Kim Morrison da0d309d65
feat: provide mergeSort comparator autoParam (#5302)
Write `mergeSort xs ys cmp` to provide an explicit comparator, or
otherwise `mergeSort xs ys` falls back to `LE` and `DecidablePred` via
an autoparam.
2024-09-12 01:50:01 +00:00
..
bench
compiler
elabissues
ir
lean feat: provide mergeSort comparator autoParam (#5302) 2024-09-12 01:50:01 +00:00
pkg
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain