[ style ] adhere to style guide

docs/src/Docs/Barbies.md

@@ -144,8 +144,9 @@ update (Just a) _ = a
 update Nothing  a = a
 
 updateUser4 : User4Update -> User4DB -> User4DB
-updateUser4 upd old = let upd' = setAt' () Int Nothing upd
-                       in hliftA2 update upd' old
+updateUser4 upd old =
+  let upd' := setAt' () Int Nothing upd
+   in hliftA2 update upd' old
 ```
 
 Let's break this down a bit: Function `setAt` replaces the
@@ -164,8 +165,10 @@ Let's see how this works out.
 ```idris
 export
 testUpd : User4DB
-testUpd = updateUser4 [Nothing,Nothing,Nothing,Just 44,Nothing]
-                      [12,"hock","[email protected]",42,"top secret"]
+testUpd =
+  updateUser4
+    [Nothing,Nothing,Nothing,Just 44,Nothing]
+    [12,"hock","[email protected]",42,"top secret"]
 ```
 
 We'll have to inspect the result at
@@ -197,11 +200,12 @@ data IdField = IdYes | IdNo
 data PasswordField = PwYes | PwNo
 
 ||| Fields of a user data type
-data UserField = Id IdField
-               | Name
-               | EMail
-               | Age
-               | PW PasswordField
+data UserField : Type where
+  Id    : IdField -> UserField
+  Name  : UserField
+  EMail : UserField
+  Age   : UserField
+  PW    : PasswordField -> UserField
 
 ||| Converts a `UserField` to the corresponding
 ||| value type
@@ -231,8 +235,9 @@ UserUpdate : Type
 UserUpdate = User IdNo PwYes Maybe
 
 updateUser : UserUpdate -> UserDB -> UserDB
-updateUser upd old = let upd' = setAt' (Id IdNo) (Id IdYes) Nothing upd
-                      in hliftA2 update upd' old
+updateUser upd old =
+  let upd' := setAt' (Id IdNo) (Id IdYes) Nothing upd
+   in hliftA2 update upd' old
 ```
 
 While the syntax is a bit more verbose that with proper

docs/src/Docs/Deriving.md

@@ -147,37 +147,45 @@ record Parser (t : Type) where
 
 public export
 Functor Parser where
-  map f pa = MkParser $ \ts => do (a,ts') <- pa.run ts
-                                  pure (f a, ts')
+  map f pa =
+    MkParser $ \ts => do
+      (a,ts') <- pa.run ts
+      pure (f a, ts')
 
 public export
 Applicative Parser where
   pure a = MkParser $ \ts => Right (a,ts)
 
-  pf <*> pa = MkParser $ \ts => do (f, ts' ) <- pf.run ts
-                                   (a, ts'') <- pa.run ts'
-                                   pure (f a, ts'')
+  pf <*> pa = MkParser $ \ts => do
+    (f, ts' ) <- pf.run ts
+    (a, ts'') <- pa.run ts'
+    pure (f a, ts'')
 
 public export
 Monad Parser where
-  pa >>= f = MkParser $ \ts => do (a, ts' ) <- pa.run ts
-                                  (f a).run ts'
+  pa >>= f = MkParser $ \ts => do
+    (a, ts' ) <- pa.run ts
+    (f a).run ts'
 
 public export
 Alternative Parser where
   empty = MkParser Left
 
-  p1 <|> p2 = MkParser $ \ts => case p1.run ts of
-                                     Left _ => p2.run ts
-                                     res    => res
+  p1 <|> p2 =
+    MkParser $ \ts =>
+      case p1.run ts of
+        Left _ => p2.run ts
+        res    => res
 
 ||| Returns the next string token, failing if
 ||| the list of tokens is empty.
 public export
 next : Parser String
-next = MkParser $ \ts => case ts of
-                              []     => Left []
-                              (h::t) => Right (h,t)
+next =
+  MkParser $ \ts =>
+    case ts of
+      []     => Left []
+      (h::t) => Right (h,t)
 
 ||| Succeeds if the next token matches exactly the
 ||| given String.
@@ -202,10 +210,11 @@ repeat p (S n) = [| p :: repeat p n |]
 ||| Fails if not the whole list is consumed.
 public export
 parse : Parser t -> List String -> Either (List String) t
-parse p ts = case p.run ts of
-                  Right (t,[]) => Right t
-                  Right (_,ts) => Left ts
-                  Left ts      => Left ts
+parse p ts =
+  case p.run ts of
+    Right (t,[]) => Right t
+    Right (_,ts) => Left ts
+    Left ts      => Left ts
 ```
 
 ### Generically derived Encoders
@@ -290,10 +299,11 @@ for all possible fields of the sum.
 Next, we define a generic version of `encode`:
 
 ```idris
-genEncode :  Generic t code
-          => POP Encode code
-          => SingletonList code
-          => t -> List String
+genEncode :
+     {auto _ : Generic t code}
+  -> {auto _ : POP Encode code}
+  -> {auto _ : SingletonList code}
+  -> t -> List String
 genEncode = encode . from
 ```
 
@@ -307,8 +317,9 @@ Encode Spell where encode = genEncode
 
 ||| The result can't be reduced any further, since `show` and
 ||| `cast` of primitives is involved.
-encodeSpellTest : encode (MkSpell 10 "foo") =
-                  [show (cast {from = Nat} {to = Integer} 10), "foo"]
+encodeSpellTest :
+  encode (MkSpell 10 "foo") =
+  [show (cast {from = Nat} {to = Integer} 10), "foo"]
 encodeSpellTest = Refl
 ```
 
@@ -351,10 +362,12 @@ Decode Double where decode = mapMaybe parseDouble next
 public export
 Decode Bool where
   decode = mapMaybe parseBool next
-    where parseBool : String -> Maybe Bool
-          parseBool "False" = Just False
-          parseBool "True"  = Just True
-          parseBool _       = Nothing
+
+    where
+      parseBool : String -> Maybe Bool
+      parseBool "False" = Just False
+      parseBool "True"  = Just True
+      parseBool _       = Nothing
 
 public export
 Decode Nat where decode = mapMaybe parsePositive next
@@ -403,10 +416,11 @@ POP (Decode . f) kss => SingletonList kss => Decode (SOP f kss) where
 And again, we provide a generic version of `decode`:
 
 ```idris
-genDecode :  Generic t code
-          => POP Decode code
-          => SingletonList code
-          => Parser t
+genDecode :
+     {auto _ : Generic t code}
+  -> {auto _ : POP Decode code}
+  -> {auto _ : SingletonList code}
+  -> Parser t
 genDecode = map to decode
 ```
 
@@ -436,9 +450,12 @@ to a dragon:
 ```idris
 public export
 gorgar : Dragon
-gorgar = MkDragon "GORGAR" 15000
-           [MkSpell 100 "Fireball", MkSpell 20 "Invisibility"]
-           ["Mail of Mithril", "1'000 gold coins"]
+gorgar =
+  MkDragon
+    "GORGAR"
+    15000
+    [MkSpell 100 "Fireball", MkSpell 20 "Invisibility"]
+    ["Mail of Mithril", "1'000 gold coins"]
 
 export
 printGorgar : IO ()

docs/src/Docs/Intro.md

@@ -107,9 +107,10 @@ Decode Double where
   decode (h::t) = Just (cast h, t)
 
 Decode a => Decode b => Decode (a,b) where
-  decode ss = do (a,ss')  <- decode ss
-                 (b,ss'') <- decode ss'
-                 pure ((a,b), ss'')
+  decode ss = do
+    (a,ss')  <- decode ss
+    (b,ss'') <- decode ss'
+    pure ((a,b), ss'')
 ```
 
 We can again define a utility function for decoding product
@@ -129,8 +130,9 @@ tupleToArticle (i,n,d,p) = MkArticle i n d p
 
 Decode Article where decode = decodeVia tupleToArticle
 
-decodeTest : Just (MkArticle 1 "foo" "bar" 10.0, Nil) =
-             decode ["1","foo","bar","10.0"]
+decodeTest :
+  Just (MkArticle 1 "foo" "bar" 10.0, Nil) =
+  decode ["1","foo","bar","10.0"]
 decodeTest = Refl
 ```
 
@@ -146,8 +148,9 @@ Idris to prove that we made no mistake:
 toTupleId : (x : Article) -> tupleToArticle (articleToTuple x) = x
 toTupleId (MkArticle _ _ _ _) = Refl
 
-fromTupleId :  (x : (Int,String,String,Double))
-            -> articleToTuple (tupleToArticle x) = x
+fromTupleId :
+     (x : (Int,String,String,Double))
+  -> articleToTuple (tupleToArticle x) = x
 fromTupleId (_,_,_,_) = Refl
 ```
 
@@ -157,9 +160,10 @@ Now that we have articles for our web store, lets define some payment
 methods we accept:
 
 ```idris
-data Payment = CreditCard String
-             | Twint String
-             | Invoice
+data Payment : Type where
+  CreditCard : String -> Payment
+  Twint      : String -> Payment
+  Invoice    : Payment
 ```
 
 Can we use the same techniques for implementing interfaces as
@@ -187,8 +191,9 @@ toEitherId (CreditCard s) = Refl
 toEitherId (Twint s)      = Refl
 toEitherId (Invoice)      = Refl
 
-fromEitherId :  (x : Either String (Either String ()))
-             -> paymentToEither (eitherToPayment x) = x
+fromEitherId :
+     (x : Either String (Either String ()))
+  -> paymentToEither (eitherToPayment x) = x
 fromEitherId (Left s)           = Refl
 fromEitherId (Right $ Left s)   = Refl
 fromEitherId (Right $ Right ()) = Refl

docs/src/Docs/Metadata.md

@@ -71,9 +71,11 @@ we can use `hcliftA2` followed by `hconcat`:
 ```idris
 genEncode : Meta t code => (all : POP Encode code) => t -> List String
 genEncode {all = MkPOP _} = encodeSOP (metaFor t) . from
-  where encodeSOP : TypeInfo code -> SOP I code -> List String
-        encodeSOP (MkTypeInfo _ _ cons) =
-          hconcat . hcliftA2 (Encode . NP I) encodeCon cons . unSOP
+
+  where
+    encodeSOP : TypeInfo code -> SOP I code -> List String
+    encodeSOP (MkTypeInfo _ _ cons) =
+      hconcat . hcliftA2 (Encode . NP I) encodeCon cons . unSOP
 ```
 
 The functions to be used in `derive` are verbatim copies of the
@@ -99,8 +101,11 @@ we somehow need to convert the decoded n-ary sum to a `SOP`
 value by applying the correct sequence of `S` and `Z` constructors:
 
 ```idris
-decodeCon :  forall ks . Decode (NP f ks)
-          => ConInfo ks -> (toSOP : NP f ks -> SOP f kss) -> Parser (SOP f kss)
+decodeCon :
+     {auto _ : Decode (NP f ks)}
+  -> ConInfo ks
+  -> (toSOP : NP f ks -> SOP f kss)
+  -> Parser (SOP f kss)
 decodeCon ci toSOP = string ci.conName *> map toSOP decode
 ```
 
@@ -115,9 +120,11 @@ the `Alternative` instance of `Parser`:
 -- Generic decoding function
 genDecode : {code : _} -> Meta t code => (all : POP Decode code) => Parser t
 genDecode {all = MkPOP _} = to <$> decodeSOP (metaFor t)
-  where decodeSOP : TypeInfo code -> Parser (SOP I code)
-        decodeSOP (MkTypeInfo _ _ cons) =
-          hchoice $ hcliftA2 (Decode . NP I) decodeCon cons injectionsSOP
+
+  where
+    decodeSOP : TypeInfo code -> Parser (SOP I code)
+    decodeSOP (MkTypeInfo _ _ cons) =
+      hchoice $ hcliftA2 (Decode . NP I) decodeCon cons injectionsSOP
 ```
 
 Again, the functions to be used in `derive` are verbatim copies of the
@@ -142,10 +149,12 @@ test them at the REPL:
 
 export
 demon : Monster
-demon = Demon { hp = 530
-              , sp = 120
-              , spells = [MkSpell 40 "Disintegrate", MkSpell 10 "Utterdark"]
-              }
+demon =
+  Demon
+    { hp = 530
+    , sp = 120
+    , spells = [MkSpell 40 "Disintegrate", MkSpell 10 "Utterdark"]
+    }
 
 export
 encDemon : List String