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/coq/hashmap/Hashmap_Funs.v | 3 ++- tests/coq/hashmap/_CoqProject | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'tests/coq/hashmap') diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index f1af0c21..b952e60c 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -9,7 +9,8 @@ Import Hashmap_Types. Module Hashmap_Funs. (** [hashmap::hash_key] *) -Definition hash_key_fwd (k : usize) : result usize := Return k. +Definition hash_key_fwd (k : usize) : result usize := + Return k. (** [hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hash_map_allocate_slots_loop_fwd diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 7f80afbf..daa9b2ba 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -3,6 +3,6 @@ -arg -w -arg all -Hashmap_Types.v Primitives.v +Hashmap_Types.v Hashmap_Funs.v -- cgit v1.2.3