summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2023-07-20 11:38:55 +0200
committerSon Ho2023-07-20 11:38:55 +0200
commitd87e35e1a53b2252cc2c8c554216115773fd9678 (patch)
treed9cca70180ca7cbbac868a9ca362fdea3c07d17b /backends/lean/Base/Progress
parent975b7c555cbffef2648a6469b777d1f1760d926d (diff)
Add fine-grained lemmas for the arithmetic operations
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Base.lean2
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 :=