lean4-htt/tests
Kim Morrison 33afaa061e
feat: improve 'apply' unification error message (#8261)
This PR adjusts the error message when `apply` fails to unify. It is
clearer about distinguishing the term being applied and the goal, as
well as distinguishing the "conclusion" of the given term and the term
itself.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
2025-05-08 16:00:42 +00:00
..
bench chore: robustify Nix shell (#8141) 2025-04-28 15:08:32 +00:00
compiler feat: wait on dedicated tasks after main is finished (#7958) 2025-04-14 11:53:54 +00:00
elabissues
ir
lean feat: improve 'apply' unification error message (#8261) 2025-05-08 16:00:42 +00:00
pkg feat: lean --setup (#8024) 2025-05-03 23:57:37 +00:00
playground chore: adjust BEq classes (#7855) 2025-04-16 13:24:23 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain