Commit 2024-09-05 05:04 9612ce14

fix: make mkRichHCongr reduce at default transparency (#16121) Without this, with_reducible congr! could fail because getFunInfoNArgs always operates at default transparency, and the assumption is that mkRichHCongr will see the same arity as recorded in the resulting FunInfo. The fix is to use whnfD instead of whnf when creating the double telescope.