whitespace fix

Author: marcinjangrzybowski

Cubical/Data/Int/Fast/Divisibility.agda

@@ -347,7 +347,7 @@ private
 quotRemPosPos : (m n : ℕ)(¬z : ¬ pos m ≡ 0) → QuotRem (pos m) (pos n)
 quotRemPosPos m n _ .div = pos (quotient  n / m)
 quotRemPosPos m n _ .rem = pos (remainder n / m)
-quotRemPosPos m n _ .quotEq =   
+quotRemPosPos m n _ .quotEq =
     (λ t → pos (≡remainder+quotient m n (~ t))) ∙ ℤ!
 quotRemPosPos 0       n ¬z .normIneq = Empty.rec (¬z refl)
 quotRemPosPos (suc m) n ¬z .normIneq = dec-helper (discreteℤ _ 0) (mod< m n)

Cubical/Data/Int/Fast/Order.agda

@@ -246,14 +246,14 @@ isTrans≤ : m ≤ n → n ≤ o → m ≤ o
 isTrans≤ {m} {n} {o} (i , p) (j , q) .fst = i ℕ.+ j
 isTrans≤ {m} {n} {o} (i , p) (j , q) .snd =
 
-  ℤ! ∙∙ cong (ℤ._+ pos j) p ∙∙ q 
+  ℤ! ∙∙ cong (ℤ._+ pos j) p ∙∙ q
 
 isAntisym≤ : m ≤ n → n ≤ m → m ≡ n
 isAntisym≤ {m} {n} (i , p) (j , q) =
   sym (+IdR _) ∙ cong ((m ℤ.+_) ∘ pos) (injPos lemma₂) ∙ p
   where lemma₀ : pos (j ℕ.+ i) ℤ.+ m ≡ m
         lemma₀ = ℤ! ∙ cong (pos j ℤ.+_) p ∙∙ +Comm (pos j) n ∙∙ q
-        
+
         lemma₁ : pos (j ℕ.+ i) ≡ 0
         lemma₁ = n+z≡z→n≡0 (pos (j ℕ.+ i)) m lemma₀
 
@@ -289,7 +289,7 @@ isAntisym≤ {m} {n} (i , p) (j , q) =
 
 <-·o : m < n → m ℤ.· (pos (suc k)) < n ℤ.· (pos (suc k))
 <-·o {m} {n} {k} (i , p) .fst = i ℕ.· suc k ℕ.+ k
-<-·o {m} {n} {k} (i , p) .snd = ℤ! ∙ cong (ℤ._· pos _) p 
+<-·o {m} {n} {k} (i , p) .snd = ℤ! ∙ cong (ℤ._· pos _) p
 
 <-o+-cancel : o ℤ.+ m < o ℤ.+ n → m < n
 <-o+-cancel {o} {m} {n} (l , p) = l , (ℤ! ∙∙ cong (ℤ._- o) p ∙∙ ℤ!)
@@ -314,7 +314,7 @@ pos≤0→≡0 {suc k} p = ⊥.rec (¬-pos<-zero {k = k} p)
 
 predℤ-≤-predℤ : m ≤ n → predℤ m ≤ predℤ n
 predℤ-≤-predℤ {m} {n} (i , p) .fst = i
-predℤ-≤-predℤ {m} {n} (i , p) .snd = ℤ! ∙ cong predℤ p 
+predℤ-≤-predℤ {m} {n} (i , p) .snd = ℤ! ∙ cong predℤ p
 
 ¬m+posk<m : ¬ m ℤ.+ pos k < m
 ¬m+posk<m {m} {k} = ¬-pos<-zero ∘ <-o+-cancel {o = m} {m = pos k} {n = 0}

Cubical/Data/Rationals/Fast/Order.agda

@@ -233,7 +233,7 @@ module _ where
                     (subst2 ℤ._≤_
                       (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
                       (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
-                      (ℤ.≤-·o {c ℤ.· ℕ₊₁→ℤ f} {k = ℕ₊₁→ℕ b} cf≤ed))))) 
+                      (ℤ.≤-·o {c ℤ.· ℕ₊₁→ℤ f} {k = ℕ₊₁→ℕ b} cf≤ed)))))
 
   isTrans< : isTrans _<_
   isTrans< =
@@ -335,7 +335,7 @@ module _ where
                         {z = c ℤ.· ℕ₊₁→ℤ b ℤ.· ℤ.pos (ℕ₊₁→ℕ f ℕ.· ℕ₊₁→ℕ f) ℤ.+
                               e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f}
                               {w = (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ℤ.· ℕ₊₁→ℤ (b ·₊₁ f)}
-                              ℤ._≤_ 
+                              ℤ._≤_
                        ℤ! ℤ!
                        (ℤ.≤-+o {a ℤ.· ℕ₊₁→ℤ d ℤ.· ℤ.pos (ℕ₊₁→ℕ f ℕ.· ℕ₊₁→ℕ f)}
                                {o = e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f}

Cubical/Data/Rationals/Fast/Order/Properties.agda

@@ -765,15 +765,15 @@ invℚ₊Dist· = uncurry (flip ∘ uncurry ∘ ElimProp2.go w)
 
 /4₊≡/2₊/2₊ : ∀ ε → fst (/4₊ ε) ≡ fst (/2₊ (/2₊ ε))
 /4₊≡/2₊/2₊ = uncurry (ElimProp.go w)
- where 
+ where
  w : ElimProp _
  w .ElimProp.isPropB _ = isPropΠ λ _ → isSetℚ _ _
  w .ElimProp.f (pos (suc n) , _)  _ = eq/ _ _ ℤ!
 
 weak0< : ∀ q (ε δ : ℚ₊)
              →  q < (fst ε - fst δ)
              → q < fst ε
-weak0< q ε δ x = 
+weak0< q ε δ x =
   let z = <Monotone+ q (fst ε - fst δ) 0 (fst δ) x (0<→< (fst δ) (snd δ))
    in subst2 _<_
        (+IdR q) ℚ! z
@@ -783,7 +783,7 @@ weak0< q ε δ x =
 weak0<' : ∀ q (ε δ : ℚ₊)
              → - (fst ε - fst δ) < q
              → - (fst ε) < q
-weak0<' q ε δ x = 
+weak0<' q ε δ x =
   let z = <Monotone+ (- (fst ε - fst δ)) q (- fst δ) 0 x
            (minus-< 0 (fst δ) ((0<→< (fst δ) (snd δ))))
   in (subst2 {x = (- (fst ε - fst δ)) + (- fst δ)}
@@ -1146,7 +1146,7 @@ riseQandD p q r =
                  (cong (_·₊₁ c') (sym (·₊₁-assoc a' b' c')
                      ∙∙ cong (a' ·₊₁_) (·₊₁-comm b' c') ∙∙ (·₊₁-assoc a' c' b'))
                     ∙ sym (·₊₁-assoc (a' ·₊₁ c') b' c')))
-                    -- 
+                    --
 
 
 <MonotoneMax : ∀ m o n s → m < n → o < s → max m o < max n s
@@ -1567,8 +1567,8 @@ maxWithPos ε q .snd = <→0< (max (fst ε) q)
                   ℤ.·Comm (snd
                             (ℤ.0<→ℕ₊₁ (pos (suc x) ℤ.· pos (suc y))
                              (·0< [ pos (suc x) , (1+ x') ] [ pos (suc y) , (1+ y') ] p' q'))
-                            (~ i1)) (pos (ℕ₊₁→ℕ ((1+ y') ·₊₁ (1+ x'))))) ∙ 
-              ℤ! 
+                            (~ i1)) (pos (ℕ₊₁→ℕ ((1+ y') ·₊₁ (1+ x'))))) ∙
+              ℤ!
                ∙ λ i → (ℕ₊₁→ℤ (fst (ℤ.0<→ℕ₊₁
                 (ℕ₊₁→ℤ ((1+ x') ·₊₁ (1+ y'))) tt))
             ℤ.· ((pos (suc y) ℤ.· ℕ₊₁→ℤ (·₊₁-identityˡ (1+ x') (~ i)))

Cubical/Tactics/CommRingSolver/IntReflection.agda

@@ -36,7 +36,7 @@ import Cubical.Data.Int.Fast as ℤ
 import Cubical.Data.Nat as ℕ
 
 import Cubical.Algebra.CommRing.Instances.Int.Fast as Fast
- 
+
 private
   variable
     ℓ : Level
@@ -111,7 +111,7 @@ private
   printVars : Vars → TC _
   printVars [] = returnTC tt
   printVars (x ∷ xs) = do
-    debugPrint "intSolver" 20 [ termErr x ] 
+    debugPrint "intSolver" 20 [ termErr x ]
     printVars xs
 
 module pr (R : CommRing ℓ) {n : ℕ} where
@@ -180,20 +180,20 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   polynomialVariable n = con (quote ∣) (finiteNumberAsTerm n v∷ [])
 
   buildExpressionFromNatLit : ℕ → TC (Template × Vars)
-  buildExpressionFromNatLit ℕ.zero = `0` [] 
+  buildExpressionFromNatLit ℕ.zero = `0` []
   buildExpressionFromNatLit (ℕ.suc ℕ.zero) = `1` []
   buildExpressionFromNatLit (ℕ.suc (ℕ.suc k)) = do
     (k' , _) ← buildExpressionFromNatLit (ℕ.suc k)
     returnTC ((λ ass → con (quote _+'_) (def (quote 1') (cring v∷ []) v∷ k' ass v∷ [])) ,
              [])
-   
+
   buildExpressionFromNat : Term → TC (Template × Vars)
   buildExpressionFromNat (lit (nat x)) = buildExpressionFromNatLit x
   buildExpressionFromNat (con (quote ℕ.zero) []) = `0` []
   buildExpressionFromNat (con (quote ℕ.suc) (con (quote ℕ.zero) [] v∷ [] )) = `1` []
   buildExpressionFromNat (con (quote ℕ.suc) (x v∷ [] )) =
     do
-    debugPrint "intSolver" 20  (strErr "fromNat suc:" ∷ termErr x ∷ []) 
+    debugPrint "intSolver" 20  (strErr "fromNat suc:" ∷ termErr x ∷ [])
     r1 ← `1` []
     r2 ← buildExpressionFromNat x
     returnTC ((λ ass → con (quote _+'_) (fst r1 ass v∷ fst r2 ass v∷ [])) ,
@@ -224,7 +224,7 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   buildExpressionFromNat t' =
    let t = (con (quote ℤ.pos) (t' v∷ []))
    in (returnTC ((λ ass → polynomialVariable (ass t)) , t ∷ []))
-  
+
   buildExpression v@(var _ _) =
     returnTC ((λ ass → polynomialVariable (ass v)) ,
              v ∷ [])
@@ -241,7 +241,7 @@ module CommRingReflection (cring : Term) (names : RingNames) where
     debugPrint "intSolver" 20  (strErr "buildExpr pos:" ∷ termErr x ∷ [])
     buildExpressionFromNat x
   buildExpression t@(con (quote ℤ.negsuc) (x v∷ [])) =
-   do debugPrint "intSolver" 20  (strErr "buildExpr negsuc:" ∷ termErr x ∷ [])    
+   do debugPrint "intSolver" 20  (strErr "buildExpr negsuc:" ∷ termErr x ∷ [])
       y ← do r1 ← `1` []
              r2 ← buildExpressionFromNat x
              returnTC {A = Template × Vars} ((λ ass → con (quote _+'_) (fst r1 ass v∷ fst r2 ass v∷ [])) ,
@@ -272,7 +272,7 @@ module CommRingReflection (cring : Term) (names : RingNames) where
   toAlgebraExpressionLHS : Term → TC (Term × Vars)
   toAlgebraExpressionLHS lhs = do
       (e , vars) ← buildExpression lhs
-      
+
       returnTC (
         let ass : VarAss
             ass n = indexOf n vars
@@ -298,7 +298,7 @@ private
           nothing
             → typeError(strErr "The CommRingSolver failed to parse the goal "
                                ∷ termErr goal ∷ [])
-      
+
       (lhs' , rhs' , vars) ← CommRingReflection.toAlgebraExpression commRing names (lhs , rhs)
       printVars vars
       let solution = solverCallWithVars (length vars) vars commRing lhs' rhs'
@@ -319,10 +319,10 @@ private
           nothing
             → typeError(strErr "The CommRingSolver failed to parse the goal "
                                ∷ termErr goal ∷ [])
-      
+
       (lhs' , vars) ← CommRingReflection.toAlgebraExpressionLHS commRing names lhs
       printVars vars
-      let solution = normaliserCallWithVars (length vars) vars commRing lhs' 
+      let solution = normaliserCallWithVars (length vars) vars commRing lhs'
       unify hole solution
 
 

Cubical/Tactics/CommRingSolver/Solver.agda

@@ -148,6 +148,6 @@ solve R = EqualityToNormalform.solve R
 
 normaliseRing : (R : CommRing ℓ)
         {n : ℕ} (e₁ : ℤExpr R n) (xs : Vec (fst R) n)
-        
+
         → _
 normaliseRing R {n} e xs  = sym (EqualityToNormalform.isEqualToNormalform R e xs)