From 75a402b9b8a4746071685d581bd0a3680f363b71 Mon Sep 17 00:00:00 2001 From: TomasPuverle Date: Sun, 22 Sep 2024 16:41:35 -0700 Subject: [PATCH] Update tests/lean/run/repr_empty.lean Updating style as per PR feedback. --- tests/lean/run/repr_empty.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/repr_empty.lean b/tests/lean/run/repr_empty.lean index 1095a1a974dc..8d917ce97497 100644 --- a/tests/lean/run/repr_empty.lean +++ b/tests/lean/run/repr_empty.lean @@ -26,4 +26,4 @@ open Prim in /-- info: Prim.minus -/ #guard_msgs in open Prim in -#eval (minus: Prim Empty) +#eval (minus : Prim Empty)