max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add notNot?

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-17 10:29:40 -07:00
parent 60ff468a8b
commit 4635c3afd1
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Util/Recognizers.lean
View file

@ -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