From d87e35e1a53b2252cc2c8c554216115773fd9678 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 11:38:55 +0200
Subject: Add fine-grained lemmas for the arithmetic operations

---
 backends/lean/Base/Progress/Base.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/lean/Base/Progress')

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 :=
-- 
cgit v1.2.3