From d36736fa4e7eb9f42f35303b8080d17ddbee92d2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:52 +0200
Subject: Revert "Update the scalar notation for the Lean backend"

This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
---
 compiler/ExtractTypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 5446f912..15e75da2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -40,7 +40,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
               let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt iname
+              F.pp_print_string fmt ("#" ^ iname)
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
-- 
cgit v1.2.3