From cd4f1968429a2ab9f4aeb0dcc5f9984280ae35cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Apr 2018 17:19:11 -0700 Subject: [PATCH] chore(library/init/data/option/basic): dead code --- library/init/data/option/basic.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index 014eaf009e..cfd9075157 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/basic.lean @@ -35,17 +35,6 @@ def get {α : Type u} : Π {o : option α}, is_some o → α | (some x) h := x | none h := false.rec _ $ bool.ff_ne_tt h -def rhoare {α : Type u} : bool → α → option α -| tt a := none -| ff a := some a - -def lhoare {α : Type u} : α → option α → α -| a none := a -| _ (some b) := b - -infixr `|>`:1 := rhoare -infixr `<|`:1 := lhoare - @[inline] protected def bind {α : Type u} {β : Type v} : option α → (α → option β) → option β | none b := none | (some a) b := b a