Commit 2023-03-06 05:18 d20d14b7
View on Github →fix: ring
: use whnfR
when obtaining goal (#2677)
Adds whnfR
so that goals which are e.g. equalities with metadata are recognized by ring
. See zulip.
fix: ring
: use whnfR
when obtaining goal (#2677)
Adds whnfR
so that goals which are e.g. equalities with metadata are recognized by ring
. See zulip.