summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2024-06-12 14:52:34 +0200
committerSon Ho2024-06-12 14:52:34 +0200
commitc8272aeea205ca9cb36e22757473ca2a931a4933 (patch)
treeceeb07f6565b2dbd76f9b506f6a43125f47e4bdf /compiler
parent1018aa1af83e639a6b41b5650bf3b717e7f8de68 (diff)
Update the scalar notation for the Lean backend
Diffstat (limited to '')
-rw-r--r--compiler/ExtractTypes.ml2
1 files changed, 1 insertions, 1 deletions
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 ")")