[ refactoring ] Tiny changes following up the idris-lang/Idris2#830

Some zeroes in signatures, one simpler implementation and formatting.

Author: buzden

libs/base/Data/Fin.idr

@@ -229,17 +229,16 @@ namespace Equality
 
   ||| The actual proof used by cast is irrelevant
   export
-  congCast : {n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
+  congCast : {0 n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
              {0 eq1 : m = n} -> {0 eq2 : p = q} ->
              k ~~~ l ->
              cast eq1 k ~~~ cast eq2 l
   congCast eq = transitive (castEq _) (transitive eq $ symmetric $ castEq _)
 
   ||| Last is congruent wrt index equality
   export
-  congLast : {m, n : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
-  congLast {m = Z} {n = Z} eq = reflexive
-  congLast {m = S _} {n = S _} eq = FS (congLast (succInjective _ _ eq))
+  congLast : {m : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
+  congLast Refl = reflexive
 
   export
   congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l
@@ -263,7 +262,7 @@ namespace Equality
   export
   hetPointwiseIsTransport :
      {0 k : Fin m} -> {0 l : Fin n} ->
-     (eq : m === n) -> k ~~~ l -> k === rewrite eq in l
+     (0 eq : m === n) -> k ~~~ l -> k === rewrite eq in l
   hetPointwiseIsTransport Refl = homoPointwiseIsEqual
 
   export

libs/contrib/Data/Fin/Extra.idr

@@ -213,7 +213,7 @@ finToNatMultHomo {m = S _} (FS x) y = Calc $
   ~~ finToNat (y + x * y)                 ...( Refl )
   ~~ finToNat y + finToNat (x * y)        ...( finToNatPlusHomo y (x * y) )
   ~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
-  ~~ finToNat (FS x) * finToNat y         ...( Refl)
+  ~~ finToNat (FS x) * finToNat y         ...( Refl )
 
 -- Relations to `Fin`'s `last`
 
@@ -292,7 +292,7 @@ plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)
 
 export
 congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
-               (c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
+                (c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
 congPlusRight c FZ
   = transitive (plusZeroRightNeutral c)
                (symmetric $ plusZeroRightNeutral c)