From 14442718cdf281bf9a33b7f56f1c3f5c6d5dc972 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?=
 <qcdz9r6wpcbh59@gmail.com>
Date: Wed, 22 Nov 2023 07:47:01 +0700
Subject: [PATCH] Use the new function

---
 compiler/coqCodegen.ts | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/compiler/coqCodegen.ts b/compiler/coqCodegen.ts
index 148c6d8..ca4a2de 100644
--- a/compiler/coqCodegen.ts
+++ b/compiler/coqCodegen.ts
@@ -46,7 +46,7 @@ export const coqCodegen = ({ environment, procedures }: CoqCPAST): string => {
           const coqType = itemTypes
             .map((x) => (x === 'bool' ? 'bool' : 'Z'))
             .join(' * ')
-          return `if decide (name = "${name}") then ${coqType} else `
+          return `if decide (name = ${getCoqString(name)}) then ${coqType} else `
         })
         .join('') +
       'False'
@@ -68,7 +68,7 @@ export const coqCodegen = ({ environment, procedures }: CoqCPAST): string => {
                 .join(', ') +
               ')'
             const list = 'repeat ' + value + ' ' + rawLength
-            return `destruct (decide (name = "${name}")) as [h |]; [(rewrite h; simpl; exact (repeat ${value} ${rawLength})) |]; `
+            return `destruct (decide (name = ${getCoqString(name)})) as [h |]; [(rewrite h; simpl; exact (repeat ${value} ${rawLength})) |]; `
           }
         )
         .join('') +