From 3468e20e9d4ec2bad79f33ae73f2c8d11f5edb94 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 13 Sep 2018 17:41:00 -0400 Subject: Add option_beq --- src/Util/Option.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util') diff --git a/src/Util/Option.v b/src/Util/Option.v index 2809655e4..5feaf5e8a 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -4,6 +4,8 @@ Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Notations. +Scheme Equality for option. + Definition bind {A B} (v : option A) (f : A -> option B) : option B := match v with | Some v => f v -- cgit v1.2.3