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 + ')'