diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 12:18:42 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 12:18:42 -0700 |
| commit | 5a9b73d71c2366feb2a1c0c9b81f9940247a2897 (patch) | |
| tree | 7f600be3c94219c2d1b1299a111ae042f629e972 /src/Util/PointedProp.v | |
| parent | eede58e3330749e3719c5452288ae20906c352e2 (diff) | |
Add a coercion [bool >-> option pointed_Prop]
Diffstat (limited to 'src/Util/PointedProp.v')
| -rw-r--r-- | src/Util/PointedProp.v | 3 |
1 files changed, 3 insertions, 0 deletions
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 |