Use slice.copy; fix list notation

upamanyus · Jun 30, 2024 · 7dc73da · 7dc73da
1 parent fc853eb
commit 7dc73da
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/goose.go b/goose.go
@@ -395,7 +395,7 @@ func (ctx Ctx) integerConversion(s ast.Node, x ast.Expr, width int) glang.Expr {
 
 func (ctx Ctx) copyExpr(n ast.Node, dst ast.Expr, src ast.Expr) glang.Expr {
 	e := sliceElem(ctx.typeOf(dst))
-	return glang.NewCallExpr(glang.GallinaIdent("SliceCopy"),
+	return glang.NewCallExpr(glang.GallinaIdent("slice.copy"),
 		ctx.coqTypeOfType(n, e),
 		ctx.expr(dst), ctx.expr(src))
 }

diff --git a/internal/glang/coq.go b/internal/glang/coq.go
@@ -690,7 +690,7 @@ func (le ListExpr) Coq(needs_paren bool) string {
 	for _, t := range le {
 		comps = append(comps, t.Coq(false))
 	}
-	return fmt.Sprintf("[%s]",
+	return fmt.Sprintf("[ %s ]",
 		indent(1, strings.Join(comps, "; ")))
 }