Commit 2026-07-07 14:28 72e1caf8

View on Github →

fix(Tactic/FunProp): resolve names to be unfolded (#41370) This allows using fun_prop [c] when c is in an open namespace. Additionally, an error is now thrown when a given constant does not exist.

Estimated changes