From c8272aeea205ca9cb36e22757473ca2a931a4933 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:52:34 +0200
Subject: Update the scalar notation for the Lean backend

---
 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 15e75da2..5446f912 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