leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: Is there code for X?

Topic: Monadic not


Paul Lezeau (Nov 27 2025 at 12:15):

Does something along the lines of this already exist?

def monadic_not {m : Type → Type} [Monad m] (x : m Bool) : m Bool :=
  Bool.not <$> x

Aaron Liu (Nov 27 2025 at 12:16):

docs#notM

Paul Lezeau (Nov 27 2025 at 12:20):

cheers!


Last updated: Dec 20 2025 at 21:32 UTC

Theme Simple by wildflame © 2016 Powered by jekyll