Update unconditional assignment optimization

Now is #t == #t with `bool-to-prop' pass

1 files changed, 8 insertions, 6 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index 11e6b5c..18f6833 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -192,23 +192,25 @@
       (newline)
       (for-each
        (lambda (rule i)
-         (if (equal? #t (body rule))
-             ;; Special case where the fact is true unconditionally.
-             (format #t "| rule~a : (~a = (~a)) → ~a ~a"
+         (match (body rule)
+           ;; Special case where the fact is true unconditionally.
+           (($ <lean-compare> 'eq ($ <constant> #t) ($ <constant> #t))
+            (format #t "| rule~a : (~a = (~a)) → ~a ~a"
                      (number->subscript i) ; rule~a
                      (subject x)           ; (~a = ~a)
                      (compile (conclusion rule))
                      inductive-name     ; → ~a
                      (subject x)
-                     )
-             (format #t "| rule~a : ~a → (~a = (~a)) → ~a ~a"
+                     ))
+           (_
+            (format #t "| rule~a : ~a → (~a = (~a)) → ~a ~a"
                      (number->subscript i) ; rule~a
                      (compile (body rule)) ; ~a →
                      (subject x)           ; (~a = ~a)
                      (compile (conclusion rule))
                      inductive-name     ; → ~a
                      (subject x)
-                     ))
+                     )))
          (newline))
        (facts x)
        (iota (length (facts x)))))))