diff options
Diffstat (limited to 'backends/lean/Base/Progress')
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 3599d866..2fbd24dd 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -240,7 +240,7 @@ initialize pspecClassExprAttr : PSpecClassExprAttr ← do -- We store two bindings: -- - arg to theorem name -- - reduced arg to theorem name - let rarg ← MetaM.run' (reduce arg) + let rarg ← MetaM.run' (reduceAll arg) trace[Progress] "Registering class spec theorem for ({fName}, {arg}) and ({fName}, {rarg})" -- Update the entry if there is one, add an entry if there is none let env := |