From e86fe3f98dbc7953c0f37c020359cc91ff263e8e Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Tue, 26 Jan 2021 00:38:07 +0200 Subject: Inlined modules are valid verilog, use correct clk --- src/common/Vericertlib.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/common/Vericertlib.v') diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index d9176db..8b56c7d 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -221,6 +221,15 @@ Definition join {A : Type} (a : option (option A)) : option A := | Some a' => a' end. +Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B := + match l with + | nil => nil + | x::xs => match f x with + | None => map_option f xs + | Some x' => x'::map_option f xs + end + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). -- cgit