From ba47a28dde13eeb0b476cf5b994d67756a94fe04 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Apr 2018 17:25:41 -0700 Subject: [PATCH] chore(library/init/category/state): remove unnecessary assumption cc @kha --- library/init/category/state.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/category/state.lean b/library/init/category/state.lean index ce8d244904..7a41681661 100644 --- a/library/init/category/state.lean +++ b/library/init/category/state.lean @@ -105,7 +105,7 @@ instance monad_state_trans {n : Type u → Type w} [has_monad_lift m n] [monad_s instance [monad m] : monad_state σ (state_t σ m) := ⟨λ α x, ⟨λ s, pure (x.run s)⟩⟩ -variables [monad m] [monad_state σ m] +variables [monad_state σ m] /-- Obtain the top-most state of a monad stack. -/ @[inline] def get : m σ :=