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.