Commit 2023-06-19 05:31 c479f374

fix: use withMainContext in borelize tactic (#5237) Also make it use withoutRecover when elaborating arguments (like in apply), and in addition use exprToSyntax to make sure each argument is elaborated only once. Adding withMainContext fixes the bug reported by @urkud on Zulip.