From 4635c3afd187147b9582d49d12231a184007dd98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Aug 2021 10:29:40 -0700
Subject: [PATCH] chore: add `notNot?`

---
 src/Lean/Util/Recognizers.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean
index a3fd604b0b..5df6fb7d9c 100644
--- a/src/Lean/Util/Recognizers.lean
+++ b/src/Lean/Util/Recognizers.lean
@@ -49,6 +49,11 @@ namespace Expr
 @[inline] def not? (p : Expr) : Option Expr :=
   p.app1? ``Not
 
+@[inline] def notNot? (p : Expr) : Option Expr :=
+  match p.not? with
+  | some p => p.not?
+  | none => none
+
 @[inline] def and? (p : Expr) : Option (Expr × Expr) :=
   p.app2? ``And