style: IsLawfulTraversable -> LawfulTraversable (#5737)

Mathlib/Algebra/Free.lean

@@ -268,7 +268,7 @@ theorem mul_map_seq (x y : FreeMagma α) :
 #align free_magma.mul_map_seq FreeMagma.mul_map_seq
 
 @[to_additive]
-instance : IsLawfulTraversable FreeMagma.{u} :=
+instance : LawfulTraversable FreeMagma.{u} :=
   { instLawfulMonadFreeMagmaInstMonadFreeMagma with
     id_traverse := fun x ↦
       FreeMagma.recOnPure x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by
@@ -684,7 +684,7 @@ theorem mul_map_seq (x y : FreeSemigroup α) :
 #align free_semigroup.mul_map_seq FreeSemigroup.mul_map_seq
 
 @[to_additive]
-instance : IsLawfulTraversable FreeSemigroup.{u} :=
+instance : LawfulTraversable FreeSemigroup.{u} :=
   { instLawfulMonadFreeSemigroupInstMonadFreeSemigroup with
     id_traverse := fun x ↦
       FreeSemigroup.recOnMul x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by

Mathlib/Control/Bitraversable/Basic.lean

@@ -30,7 +30,7 @@ and value respectively with `Bitraverse f g : AList key val → IO (AList key' v
 
 * `Bitraversable`: Bare typeclass to hold the `Bitraverse` function.
 * `LawfulBitraversable`: Typeclass for the laws of the `Bitraverse` function. Similar to
-  `IsLawfulTraversable`.
+  `LawfulTraversable`.
 
 ## References
 

Mathlib/Control/Bitraversable/Instances.lean

@@ -103,7 +103,7 @@ instance (priority := 10) Bitraversable.traversable {α} : Traversable (t α) wh
 #align bitraversable.traversable Bitraversable.traversable
 
 instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable t] {α} :
-    IsLawfulTraversable (t α) := by
+    LawfulTraversable (t α) := by
   constructor <;> intros <;>
     simp [traverse, comp_tsnd, functor_norm, -ApplicativeTransformation.app_eq_coe]
   · simp [tsnd_eq_snd_id]; rfl
@@ -112,7 +112,7 @@ instance (priority := 10) Bitraversable.isLawfulTraversable [LawfulBitraversable
 
 end
 
-open Bifunctor Traversable IsLawfulTraversable LawfulBitraversable
+open Bifunctor Traversable LawfulTraversable LawfulBitraversable
 
 open Function (bicompl bicompr)
 
@@ -128,7 +128,7 @@ nonrec def Bicompl.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m
 
 instance : Bitraversable (bicompl t F G) where bitraverse := @Bicompl.bitraverse t _ F G _ _
 
-instance [IsLawfulTraversable F] [IsLawfulTraversable G] [LawfulBitraversable t] :
+instance [LawfulTraversable F] [LawfulTraversable G] [LawfulBitraversable t] :
     LawfulBitraversable (bicompl t F G) := by
   constructor <;> intros <;>
     simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
@@ -151,7 +151,7 @@ nonrec def Bicompr.bitraverse {m} [Applicative m] {α β α' β'} (f : α → m
 
 instance : Bitraversable (bicompr F t) where bitraverse := @Bicompr.bitraverse t _ F _
 
-instance [IsLawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) := by
+instance [LawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (bicompr F t) := by
   constructor <;> intros <;>
     simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm,
       -ApplicativeTransformation.app_eq_coe]

Mathlib/Control/Fold.lean

@@ -277,9 +277,9 @@ theorem foldl.unop_ofFreeMonoid (f : β → α → β) (xs : FreeMonoid α) (a :
 
 variable (m : Type u → Type u) [Monad m] [LawfulMonad m]
 
-variable {t : Type u → Type u} [Traversable t] [IsLawfulTraversable t]
+variable {t : Type u → Type u} [Traversable t] [LawfulTraversable t]
 
-open IsLawfulTraversable
+open LawfulTraversable
 
 theorem foldMap_hom [Monoid α] [Monoid β] (f : α →* β) (g : γ → α) (x : t γ) :
     f (foldMap g x) = foldMap (f ∘ g) x :=
@@ -299,13 +299,13 @@ end ApplicativeTransformation
 
 section Equalities
 
-open IsLawfulTraversable
+open LawfulTraversable
 
 open List (cons)
 
 variable {α β γ : Type u}
 
-variable {t : Type u → Type u} [Traversable t] [IsLawfulTraversable t]
+variable {t : Type u → Type u} [Traversable t] [LawfulTraversable t]
 
 @[simp]
 theorem foldl.ofFreeMonoid_comp_of (f : α → β → α) :

Mathlib/Control/Traversable/Basic.lean

@@ -38,7 +38,7 @@ For more on how to use traversable, consider the Haskell tutorial:
   * `Traversable` type class - exposes the `traverse` function
   * `sequence` - based on `traverse`,
     turns a collection of effects into an effect returning a collection
-  * `IsLawfulTraversable` - laws for a traversable functor
+  * `LawfulTraversable` - laws for a traversable functor
   * `ApplicativeTransformation` - the notion of a natural transformation for applicative functors
 
 ## Tags
@@ -250,7 +250,7 @@ send the composition of applicative functors to the composition of the
 `traverse` of each, send each function `f` to `fun x ↦ f <$> x`, and
 satisfy a naturality condition with respect to applicative
 transformations. -/
-class IsLawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor t :
+class LawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor t :
     Type (u + 1) where
   /-- `traverse` plays well with `pure` of the identity monad-/
   id_traverse : ∀ {α} (x : t α), traverse (pure : α → Id α) x = x
@@ -268,12 +268,12 @@ class IsLawfulTraversable (t : Type u → Type u) [Traversable t] extends Lawful
     ∀ {F G} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G]
       (η : ApplicativeTransformation F G) {α β} (f : α → F β) (x : t α),
       η (traverse f x) = traverse (@η _ ∘ f) x
-#align is_lawful_traversable IsLawfulTraversable
+#align is_lawful_traversable LawfulTraversable
 
 instance : Traversable Id :=
   ⟨id⟩
 
-instance : IsLawfulTraversable Id := by refine' { .. } <;> intros <;> rfl
+instance : LawfulTraversable Id := by refine' { .. } <;> intros <;> rfl
 
 section
 

Mathlib/Control/Traversable/Equiv.lean

@@ -118,9 +118,8 @@ section Equiv
 
 variable {t t' : Type u → Type u} (eqv : ∀ α, t α ≃ t' α)
 
--- Porting note: The naming `IsLawfulTraversable` seems weird, why not `LawfulTraversable`?
 -- Is this to do with the fact it lives in `Type (u+1)` not `Prop`?
-variable [Traversable t] [IsLawfulTraversable t]
+variable [Traversable t] [LawfulTraversable t]
 
 variable {F G : Type u → Type u} [Applicative F] [Applicative G]
 
@@ -130,7 +129,7 @@ variable (η : ApplicativeTransformation F G)
 
 variable {α β γ : Type u}
 
-open IsLawfulTraversable Functor
+open LawfulTraversable Functor
 
 -- Porting note: Id.bind_eq is missing an `#align`.
 
@@ -158,7 +157,7 @@ protected theorem naturality (f : α → F β) (x : t' α) :
 /-- The fact that `t` is a lawful traversable functor carries over the
 equivalences to `t'`, with the traversable functor structure given by
 `Equiv.traversable`. -/
-protected def isLawfulTraversable : @IsLawfulTraversable t' (Equiv.traversable eqv) :=
+protected def isLawfulTraversable : @LawfulTraversable t' (Equiv.traversable eqv) :=
   -- Porting note: Same `_inst` local variable problem.
   let _inst := Equiv.traversable eqv; {
     toLawfulFunctor := Equiv.lawfulFunctor eqv
@@ -179,7 +178,7 @@ protected def isLawfulTraversable' [Traversable t']
     (h₂ :
       ∀ {F : Type u → Type u} [Applicative F],
         ∀ [LawfulApplicative F] {α β} (f : α → F β), traverse f = Equiv.traverse eqv f) :
-    IsLawfulTraversable t' := by
+    LawfulTraversable t' := by
   -- we can't use the same approach as for `lawful_functor'` because
   -- h₂ needs a `LawfulApplicative` assumption
   refine' { toLawfulFunctor := Equiv.lawfulFunctor' eqv @h₀ @h₁.. } <;> intros

Mathlib/Control/Traversable/Instances.lean

@@ -14,9 +14,9 @@ import Mathlib.Data.List.Forall2
 import Mathlib.Data.Set.Functor
 
 /-!
-# IsLawfulTraversable instances
+# LawfulTraversable instances
 
-This file provides instances of `IsLawfulTraversable` for types from the core library: `Option`,
+This file provides instances of `LawfulTraversable` for types from the core library: `Option`,
 `List` and `Sum`.
 -/
 
@@ -58,7 +58,7 @@ theorem Option.naturality {α β} (f : α → F β) (x : Option α) :
 
 end Option
 
-instance : IsLawfulTraversable Option :=
+instance : LawfulTraversable Option :=
   { show LawfulMonad Option from inferInstance with
     id_traverse := Option.id_traverse
     comp_traverse := Option.comp_traverse
@@ -100,7 +100,7 @@ protected theorem naturality {α β} (f : α → F β) (x : List α) :
     ApplicativeTransformation.preserves_seq, ApplicativeTransformation.preserves_pure]
 #align list.naturality List.naturality
 
-instance : IsLawfulTraversable.{u} List :=
+instance : LawfulTraversable.{u} List :=
   { show LawfulMonad List from inferInstance with
     id_traverse := List.id_traverse
     comp_traverse := List.comp_traverse
@@ -195,7 +195,7 @@ protected theorem naturality {α β} (f : α → F β) (x : σ ⊕ α) :
 
 end Traverse
 
-instance {σ : Type u} : IsLawfulTraversable.{u} (Sum σ) :=
+instance {σ : Type u} : LawfulTraversable.{u} (Sum σ) :=
   { show LawfulMonad (Sum σ) from inferInstance with
     id_traverse := Sum.id_traverse
     comp_traverse := Sum.comp_traverse

Mathlib/Control/Traversable/Lemmas.lean

@@ -25,21 +25,21 @@ Inspired by [The Essence of the Iterator Pattern][gibbons2009].
 
 universe u
 
-open IsLawfulTraversable
+open LawfulTraversable
 
 open Function hiding comp
 
 open Functor
 
-attribute [functor_norm] IsLawfulTraversable.naturality
+attribute [functor_norm] LawfulTraversable.naturality
 
-attribute [simp] IsLawfulTraversable.id_traverse
+attribute [simp] LawfulTraversable.id_traverse
 
 namespace Traversable
 
 variable {t : Type u → Type u}
 
-variable [Traversable t] [IsLawfulTraversable t]
+variable [Traversable t] [LawfulTraversable t]
 
 variable (F G : Type u → Type u)
 

Mathlib/Data/DList/Instances.lean

@@ -38,7 +38,7 @@ def DList.listEquivDList : List α ≃ DList α := by
 instance : Traversable DList :=
   Equiv.traversable DList.listEquivDList
 
-instance : IsLawfulTraversable DList :=
+instance : LawfulTraversable DList :=
   Equiv.isLawfulTraversable DList.listEquivDList
 
 instance {α} : Inhabited (DList α) :=

Mathlib/Data/LazyList/Basic.lean

@@ -89,7 +89,7 @@ instance : Traversable LazyList where
   map := @LazyList.traverse Id _
   traverse := @LazyList.traverse
 
-instance : IsLawfulTraversable LazyList := by
+instance : LawfulTraversable LazyList := by
   apply Equiv.isLawfulTraversable' listEquivLazyList <;> intros <;> ext <;> rename_i f xs
   · induction' xs using LazyList.rec with _ _ _ _ ih
     · rfl

Mathlib/Data/Multiset/Functor.lean

@@ -32,7 +32,7 @@ theorem fmap_def {α' β'} {s : Multiset α'} (f : α' → β') : f <$> s = s.ma
 
 instance : LawfulFunctor Multiset := by refine' { .. } <;> intros <;> simp; rfl
 
-open IsLawfulTraversable CommApplicative
+open LawfulTraversable CommApplicative
 
 variable {F : Type u → Type u} [Applicative F] [CommApplicative F]
 
@@ -86,7 +86,7 @@ instance : LawfulMonad Multiset := LawfulMonad.mk'
 
 open Functor
 
-open Traversable IsLawfulTraversable
+open Traversable LawfulTraversable
 
 @[simp]
 theorem lift_coe {α β : Type _} (x : List α) (f : List α → β)
@@ -141,7 +141,7 @@ theorem naturality {G H : Type _ → Type _} [Applicative G] [Applicative H] [Co
   refine' Quotient.inductionOn x _
   intro
   simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply,
-    ApplicativeTransformation.preserves_map, IsLawfulTraversable.naturality]
+    ApplicativeTransformation.preserves_map, LawfulTraversable.naturality]
 #align multiset.naturality Multiset.naturality
 
 end Multiset

Mathlib/Data/Vector/Basic.lean

@@ -706,7 +706,7 @@ variable [LawfulApplicative F] [LawfulApplicative G]
 variable {α β γ : Type u}
 
 -- We need to turn off the linter here as
--- the `IsLawfulTraversable` instance below expects a particular signature.
+-- the `LawfulTraversable` instance below expects a particular signature.
 @[nolint unusedArguments]
 protected theorem comp_traverse (f : β → F γ) (g : α → G β) (x : Vector α n) :
     Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x =
@@ -739,7 +739,7 @@ instance : Traversable.{u} (flip Vector n) where
   traverse := @Vector.traverse n
   map {α β} := @Vector.map.{u, u} α β n
 
-instance : IsLawfulTraversable.{u} (flip Vector n) where
+instance : LawfulTraversable.{u} (flip Vector n) where
   id_traverse := @Vector.id_traverse n
   comp_traverse := Vector.comp_traverse
   traverse_eq_map_id := @Vector.traverse_eq_map_id n

Mathlib/Logic/Equiv/Array.lean

@@ -56,7 +56,7 @@ def arrayEquivList (α : Type _) : Array α ≃ List α :=
 end Equiv
 
 /- Porting note: removed instances for what would be ported as `Traversable (Array α)` and
-`IsLawfulTraversable (Array α)`. These would
+`LawfulTraversable (Array α)`. These would
 
 1. be implemented directly in terms of `Array` functionality for efficiency, rather than being the
 traversal of some other type transported along an equivalence to `Array α` (as the traversable
@@ -73,7 +73,7 @@ instance for `array` was)
 -- instance : Traversable (Array' n) :=
 --   @Equiv.traversable (flip Vector n) _ (fun α => Equiv.vectorEquivArray α n) _
 
--- instance : IsLawfulTraversable (Array' n) :=
+-- instance : LawfulTraversable (Array' n) :=
 --   @Equiv.isLawfulTraversable (flip Vector n) _ (fun α => Equiv.vectorEquivArray α n) _ _
 
 -- end Array'