From 5a9b73d71c2366feb2a1c0c9b81f9940247a2897 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 12:18:42 -0700 Subject: Add a coercion [bool >-> option pointed_Prop] --- src/Util/PointedProp.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Util/PointedProp.v') diff --git a/src/Util/PointedProp.v b/src/Util/PointedProp.v index bc9626477..55cbe6d74 100644 --- a/src/Util/PointedProp.v +++ b/src/Util/PointedProp.v @@ -14,6 +14,9 @@ Definition to_prop (x : pointed_Prop) : Prop | inject p => p end. +Coercion option_pointed_Prop_of_bool (x : bool) : option pointed_Prop + := if x then Some trivial else None. + Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop := match x, y with | trivial, y => y -- cgit v1.2.3