From afb97a1caa499c51083f804795be48a7a8e3a467 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?= Date: Sun, 3 Dec 2023 11:19:19 +0000 Subject: [PATCH] Fix --- compiler/coqCodegen.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/coqCodegen.ts b/compiler/coqCodegen.ts index 1d08d6e..bc7bb65 100644 --- a/compiler/coqCodegen.ts +++ b/compiler/coqCodegen.ts @@ -509,7 +509,7 @@ Proof. simpl. repeat destruct (decide _). all: solve_decision. Defined. return header + joinStatements(statements) + '\n' function joinStatements(statements: string[]) { - if (statements.length) return 'Done _ _ _ tt' + if (statements.length === 0) return 'Done _ _ _ tt' return statements.reduce( (accumulated, current) => 'bind (' + accumulated + ') (fun ignored => ' + current + ')'