Globally delete all trailing whitespace

Author: dunnl

Tealeaves/Backends/LN/AssocList.v

@@ -438,7 +438,7 @@ Section range_lemmas.
       range (envmap f Γ) = fmap list f (range Γ).
   Proof.
     intros. unfold range, envmap. compose near Γ.
-    unfold_ops @Fmap_compose.    
+    unfold_ops @Fmap_compose.
     rewrite (fun_fmap_fmap list _ _ _ (fmap (prod atom) f) (extract (prod atom))).
     rewrite (fun_fmap_fmap list _ _ _ (extract (prod atom)) f).
     fequal. now ext [? ?].

Tealeaves/Backends/LN/LN.v

@@ -149,7 +149,7 @@ Section locally_nameless_operations.
 
   Definition subst x (u : T LN) : T LN -> T LN :=
     bind T (subst_loc x u).
-  
+
   Definition free : T LN -> list atom :=
     fun t => bind list free_loc (tolist T t).
 
@@ -210,7 +210,7 @@ Tactic Notation "unfold_lia" :=
 Section locally_nameless_basic_principles.
 
   Import Notations.
-  
+
   Context
     `{DT.Monad.Monad nat T
      (unit := Monoid_unit_zero)

Tealeaves/Classes/DT/Monad.v

@@ -67,12 +67,12 @@ From Tealeaves Require
 Module ToKleisli.
 
   Import Classes.Kleisli.DT.Monad.
-  
+
   Import Classes.Kleisli.DT.Monad.Notations.
   Import Classes.Monad.Notations.
   Import Classes.Traversable.Functor.Notations.
   Import Data.Strength.Notations.
-  
+
   Section operation.
 
     Context
@@ -145,7 +145,7 @@ Module ToKleisli.
 
     Import Decorated.Monad.ToKleisli.
     Import Kleisli.Decorated.Monad.
-    
+
     Theorem kdtm_binddt1_T {A} : binddt T (fun A => A) (ret T ∘ extract (prod W)) = @id (T A).
     Proof.
       introv. unfold_ops @Binddt_ddj.

Tealeaves/Classes/Decorated/Functor.v

@@ -312,7 +312,7 @@ Module ToKleisli.
 
   Import Classes.Kleisli.Decorated.Functor.
   Import Comonad.Notations.
-  
+
   Section operation.
 
     Context

Tealeaves/Classes/Equivalences/Decorated/Functor.v

@@ -77,7 +77,7 @@ End properties.
 Import Kleisli.Decorated.Functor.ToFunctor.
 
 Module Roundtrip1.
-  
+
   Context
     `{fmapT : Fmap T}
     `{decT : Decorate E T}

Tealeaves/Classes/Equivalences/Decorated/Monad.v

@@ -256,7 +256,7 @@ End Instances.
 #[local] Generalizable Variables T W.
 
 Module CategoricalToKleisli.
-  
+
   Context
     `{fmapT : Fmap T}
     `{decT : Decorate W T}

Tealeaves/Classes/Equivalences/Traversable/Functor.v

@@ -101,7 +101,7 @@ Module AlgebraicToKleisli.
     `{! Traversable.Functor.TraversableFunctor T}.
 
   #[local] Instance traverse' : Traverse T := ToKleisli.Traverse_dist T.
-  
+
   Definition fmap' : Fmap T := ToFunctor.Fmap_Traverse T.
   Definition dist' : Dist T := Dist_Traverse T.
 

Tealeaves/Classes/Kleisli/Decorated/Functor.v

@@ -42,7 +42,7 @@ End class.
 (** * To functor *)
 (******************************************************************************)
 Module ToFunctor.
-  
+
   Section operation.
 
     Context

Tealeaves/Classes/Kleisli/Decorated/Monad.v

@@ -176,15 +176,15 @@ End kleisli_composition.
 From Tealeaves Require Import
   Classes.Kleisli.Monad
   Classes.Kleisli.Decorated.Functor.
-  
+
 (** * Derived instances *)
 (******************************************************************************)
 Module Derived.
 
   Import
     Kleisli.Monad.Notations
     Comonad.Notations.
-  
+
   Section operations.
 
     Context
@@ -197,7 +197,7 @@ Module Derived.
     #[export] Instance Fmapd_Bindd: Fmapd W T := fun A B f => bindd T (ret T ∘ f).
 
   End operations.
-  
+
   (** ** Lesser Kleisli composition laws *)
   (******************************************************************************)
   Section Kleisli_composition.
@@ -304,9 +304,9 @@ Module Derived.
     Qed.
 
   End with_monad.
-  
+
   Section laws.
-    
+
     Context
       (T : Type -> Type)
       `{Decorated.Monad.Monad W T}.
@@ -383,5 +383,5 @@ Module Derived.
     (******************************************************************************)
 
   End laws.
-  
+
 End Derived.

Tealeaves/Classes/Kleisli/Monad.v

@@ -16,7 +16,7 @@ Section kleisli_operations.
     (F T : Type -> Type).
 
   Class Return := ret : (fun A => A) ⇒ T.
-  
+
   Class Bind :=
     bind : forall (A B : Type), (A -> T B) -> F A -> F B.
 

Tealeaves/Classes/Kleisli/Traversable/Functor.v

@@ -53,7 +53,7 @@ End class.
 (** ** <<Functor>> instance *)
 (******************************************************************************)
 Module ToFunctor.
-  
+
   Section operation.
 
     Context
@@ -64,7 +64,7 @@ Module ToFunctor.
       fun (A B : Type) (f : A -> B) => traverse T (fun A => A) f.
 
   End operation.
-  
+
   Section properties.
 
     Context
@@ -149,7 +149,7 @@ Module ToFunctor.
     Qed.
 
   End properties.
-  
+
 End ToFunctor.
 
 Import Batch.Notations.

Tealeaves/Classes/Kleisli/Traversable/Monad.v

@@ -121,7 +121,7 @@ Module Derived.
       fun G _ _ _ A B f => bindt T G (fmap G (ret T) ∘ f).
 
   End operations.
-  
+
   Section special_cases.
 
     Context
@@ -207,7 +207,7 @@ Module Derived.
       {| fun_fmap_id := fmap_id;
         fun_fmap_fmap := fmap_fmap;
       |}.
-    
+
     (** *** Monad instance *)
     (******************************************************************************)
     #[export] Instance: Kleisli.Monad.Monad T.
@@ -236,7 +236,7 @@ Module Derived.
     Qed.
 
   End with_kleisli.
-  
+
   (** ** Special cases for Kleisli composition *)
   (******************************************************************************)
   Section Kleisli_composition.
@@ -347,7 +347,7 @@ Module Derived.
     rewrite (fun_fmap_id T).
     now rewrite (fun_fmap_id G1).
   Qed.
-  
+
   End Kleisli_composition.
 
   (** ** Composition with lesser Kleisli operations *)
@@ -361,7 +361,7 @@ Module Derived.
       (G2 : Type -> Type)
       `{Applicative G2}
       `{Applicative G1}.
-  
+
   (** *** Composition with <<fmap>> *)
   (******************************************************************************)
   Lemma fmap_bindt : forall `(g : B -> C) `(f : A -> G1 (T B)),
@@ -382,7 +382,7 @@ Module Derived.
     fequal. now rewrite Mult_compose_identity2.
     rewrite kcompose_tm30; auto.
   Qed.
-  
+
   (** *** Composition with <<traverse>> *)
   (******************************************************************************)
   Lemma traverse_bindt : forall `(g : B -> G2 C) `(f : A -> G1 (T B)),
@@ -492,7 +492,7 @@ Module Derived.
     change (@Fmap_Bindt T H0 H) with (@ToFunctor.Fmap_Bind T _ _).
     now rewrite (ToFunctor.fmap_bind T).
   Qed.
-  
+
   End Kleisli_composition.
 
 End Derived.

Tealeaves/Classes/Listable/Monad.v

@@ -44,7 +44,7 @@ End Listable_list.
 Section listable_monad_compatibility_conditions.
 
   Generalizable All Variables.
-  
+
   Context
     `{Monad T}
     `{Tolist T}
@@ -110,7 +110,7 @@ End listable_monad_compatibility_conditions.
 (** * Properties of listable monads *)
 (******************************************************************************)
 Section ListableMonad_theory.
-  
+
   Context
     `{ListableMonad T}.
 

Tealeaves/Classes/Monad.v

@@ -85,16 +85,16 @@ Module ToKleisli.
   Generalizable All Variables.
 
   Section operation.
-    
+
     Context
       (T : Type -> Type)
       `{Fmap T} `{Join T}.
 
     #[export] Instance Bind_join : Bind T T :=
       fun {A B} (f : A -> T B) => join T ∘ fmap T f.
-    
+
   End operation.
-  
+
   Section with_monad.
 
     Context

Tealeaves/Classes/Monad/ToApplicative.v

@@ -1,18 +1,18 @@
 From Tealeaves.Classes Require Import
   Monad
   Applicative.
-  
+
 (** * Monadic applicative functors *)
 (******************************************************************************)
 Section Applicative_Monad.
 
   #[local] Generalizable Variable T.
-  
+
   Import Applicative.Notations.
-  
+
   Context
     `{Classes.Monad.Monad T}.
-  
+
   Import Monad.ToKleisli.Operation.
   Import Monad.ToKleisli.Instance.
 

Tealeaves/Classes/RightModule.v

@@ -64,7 +64,7 @@ End RightModule_Monad.
 Section functor_module_composition.
 
   #[local] Generalizable Variables F G.
-  
+
   Context
     `{Functor F}
     `{RightModule G T}.
@@ -103,14 +103,14 @@ From Tealeaves Require Import Classes.Kleisli.Monad.
 (** * Kleisli laws for <<bind>> *)
 (******************************************************************************)
 Module ToKleisli.
-  
+
   Import Kleisli.Monad.Notations.
   Import Classes.Monad.ToKleisli.
-  
+
   Section Monad_kleisli_laws.
 
     Generalizable All Variables.
-    
+
     Context
       (T : Type -> Type)
         `{Classes.RightModule.RightModule F T}.

Tealeaves/Classes/Traversable/Listable.v

@@ -40,7 +40,7 @@ Section TraversableFunctor_fold_spec.
   Context
     (T : Type -> Type)
     `{TraversableFunctor T}.
-  
+
   Import Classes.Kleisli.Traversable.Functor.
   Import Traversable.Functor.ToKleisli.
 

Tealeaves/Functors/Sets.v

@@ -159,7 +159,7 @@ Qed.
 TODO: This isn't really necessary because it is inferred from the monad instance.
  *)
 Section set_applicative.
-  
+
   Instance Pure_set : Pure set := @eq.
 
   #[export] Instance Mult_set : Mult set :=