From e4a173f4ebd46b5e3f45ee4f65a93790d68544ab Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 1 Sep 2021 14:06:51 +0100 Subject: Use sumbool instead of option for decide_ram_wf --- src/hls/HTL.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/hls/HTL.v') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 3116af3..303dc70 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -448,16 +448,16 @@ Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True} end; unfold module_ordering; auto. Defined. -Definition option_ram_wf (clk : reg) (mr : option HTL.ram) : - option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive). +Definition decide_ram_wf (clk : reg) (mr : option HTL.ram) : + {forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive} + {True}. refine ( match mr with | Some r => match (plt clk (ram_addr r)) with - | left LE => Some _ - | _ => None + | left LE => left _ + | _ => right I end - | None => None + | None => left _ end). - crush. + all: crush. Defined. -- cgit