From c6913b8bf90689d8961c47f59896443e7fae164d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 5 Feb 2023 22:03:41 +0100 Subject: Make sure let-bindings in Lean end with line breaks and improve formatting --- tests/lean/misc/loops/Loops/Funs.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tests/lean/misc/loops/Loops') diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean index 33a3a881..8b7e8a1f 100644 --- a/tests/lean/misc/loops/Loops/Funs.lean +++ b/tests/lean/misc/loops/Loops/Funs.lean @@ -221,7 +221,8 @@ def get_elem_shared_fwd get_elem_shared_loop_fwd x l /- [loops::id_mut] -/ -def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) := result.ret ls +def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) := + result.ret ls /- [loops::id_mut] -/ def id_mut_back -- cgit v1.2.3