Repository navigation

fix: don't error in defeq for missing unification hints - #14733

Open

Rob23oba wants to merge 2 commits into

leanprover:masterfrom

Rob23oba:unif-hint-fix-private

Open

fix: don't error in defeq for missing unification hints#14733
Rob23oba wants to merge 2 commits into
leanprover:masterfrom
Rob23oba:unif-hint-fix-private

Commits on Aug 10, 2026
- fix unification hints not being imported publicly
  Rob23oba
  committed
  de69645
- add test
  Rob23oba
  committed
  32c7fde