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

fix(library/init/option): remove unused variable

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-14 15:38:09 -08:00
parent 7232e3a076
commit bd249bb1cc
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/option.lean
View file

@ -65,7 +65,7 @@ do o ← a,
show M (option A), from
return (some a)
instance {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : monad (optionT M) :=
instance {M : Type (max 1 u) → Type v} [monad M] : monad (optionT M) :=
monad.mk (@optionT_fmap M _) (@optionT_return M _) (@optionT_bind M _)
def optionT_orelse {M : Type (max 1 u) → Type v} [monad M] {A : Type u} (a : optionT M A) (b : optionT M A) : optionT M A :=
@ -80,9 +80,9 @@ def optionT_fail {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : option
show M (option A), from
return none
instance {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : alternative (optionT M) :=
instance {M : Type (max 1 u) → Type v} [monad M] : alternative (optionT M) :=
{map := @optionT_fmap M _,
pure := @optionT_return M _,
seq := @fapp (optionT M) (@optionT.monad M _ A),
seq := @fapp (optionT M) (@optionT.monad M _),
failure := @optionT_fail M _,
orelse := @optionT_orelse M _}