From 7434d3dcdb2ec35b5a5cb1b74ee4bf073a596a8e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jul 2020 16:06:59 -0700 Subject: [PATCH] test: `structure` --- tests/lean/run/struct3.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 tests/lean/run/struct3.lean diff --git a/tests/lean/run/struct3.lean b/tests/lean/run/struct3.lean new file mode 100644 index 0000000000..073ecdda9c --- /dev/null +++ b/tests/lean/run/struct3.lean @@ -0,0 +1,14 @@ +new_frontend + +universes u v + +class HasBind2 (m : Type u → Type v) := +(bind : ∀ {α β : Type u}, m α → (α → m β) → m β) + +set_option pp.all true + +class Monad2 (m : Type u → Type v) extends Applicative m, HasBind2 m : Type (max (u+1) v) := +(map := fun f x => HasBind2.bind x (pure ∘ f)) +(seq := fun f x => HasBind2.bind f fun y => Functor.map y x) +(seqLeft := fun x y => HasBind2.bind x fun a => HasBind2.bind y fun _ => pure a) +(seqRight := @fun β x y => HasBind2.bind x fun _ => y) -- Recall that `@` disables implicit lambda support