Use the new function

huynhtrankhanh · Nov 22, 2023 · 1444271 · 1444271
1 parent dfb460a
commit 1444271
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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('') +