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

test: add new structure instance + implicit lambda tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-18 09:18:52 -08:00
parent c7fcb2c5a7
commit dcd64fae5a
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
tests/lean/run/structInst2.lean Normal file
View file

@ -0,0 +1,11 @@
import Init.Control.Option
new_frontend
def optMonad {m} [Monad m] : Monad (OptionT m) :=
{ pure := OptionT.pure, bind := OptionT.bind }
def optAlt {m} [Monad m] : Alternative (OptionT m) :=
{ failure := OptionT.fail,
orelse := OptionT.orelse,
toApplicative := Monad.toApplicative (OptionT m) } -- TODO: check toApplicative binder annotations