docs(category/monad,bitraversable): add module docstrings #1260

src/category/bitraversable/instances.lean

@@ -1,8 +1,26 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+
 import category.bitraversable.basic
        category.bitraversable.lemmas
        category.traversable.lemmas
        tactic.solve_by_elim
 
+/-!
+# bitraversable instances for
+ * prod
+ * sum
+ * const
+ * flip
+ * bicompl
+ * bicompr
+
+# traversable instances for bitraversable functors
+-/
+
 universes u v w
 
 variables {t : Type u → Type u → Type u} [bitraversable t]

src/category/bitraversable/lemmas.lean

@@ -1,5 +1,25 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
+
 import category.bitraversable.basic
 
+/-!
+# specialized bitraverse
+  * tfst - traverse on first functor argument
+  * tsnd - traverse on second functor argument
+
+# properties of
+  * bitraverse
+  * tfst
+  * tsnd
+with
+  * id
+  * comp
+-/
+
 universes u
 
 variables {t : Type u → Type u → Type u} [bitraversable t]

src/category/monad/basic.lean

@@ -1,9 +1,32 @@
+/-
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Simon Hudon
+-/
 
 import tactic.basic
 
+/-!
+Set of rewrite rules and automation for monads in general and
+`reader_t`, `state_t`, `except_t` and `option_t` in particular.
+
+The rewrite rules for monads are carefully chosen so that `simp with
+functor_norm` will not introduce monadic vocabulary in a context where
+applicatives would do just fine but will handle monadic notation
+already present in an expression.
+
+In a context where monadic reasoning is desired `simp with monad_norm`
+will translate functor and applicative notation into monad notation
+and use regular `functor_norm` rules as well.
+-/
+
+run_cmd mk_simp_attr `monad_norm [`functor_norm]
+
 attribute [extensionality] reader_t.ext state_t.ext except_t.ext option_t.ext
 attribute [functor_norm]   bind_assoc pure_bind bind_pure
+attribute [monad_norm] seq_eq_bind_map
 universes u v
 
+@[monad_norm]
 lemma map_eq_bind_pure_comp (m : Type u → Type v) [monad m] [is_lawful_monad m] {α β : Type u} (f : α → β) (x : m α) :
   f <$> x = x >>= pure ∘ f := by rw bind_pure_comp_eq_map