fabian/veribase-idr2 - Change RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC

Refactor

Created by fabian on June 11, 2021

RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC

Dependencies

In channels

main

Change contents

Replacement in src/Data/Optional.idr at line 48 [7.30]

B:BD[6.380] → [6.380:439]

  map f Nothing  = Nothing
  map f (Some a) = Some . f $ a

[6.380]

[6.439]

  f <$>  Nothing = Nothing
  f <$> (Some a) = Some $ f a

Replacement in src/Data/Natural.idr at line 53 [8.31]

B:BD[8.1192] → [8.1192:1249]

      No cp => No $ proofNotEquivThenNotSuccesorEquiv cp

[8.1192]

[9.64]

      No cp => No  $ proofNotEquivThenNotSuccesorEquiv cp

Replacement in src/Data/Natural.idr at line 60 [8.31]

B:BD[9.130] → [9.130:234]

  ZeroLTEAny : NaturalLTE Zero y
  SuccesorLTE : NaturalLTE x y -> NaturalLTE (Succesor x) (Succesor y)

[9.130]

[9.234]

  ZeroLTEAny  : NaturalLTE Zero y
  SuccesorLTE : NaturalLTE x    y -> NaturalLTE (Succesor x) (Succesor y)

Replacement in src/Data/Natural.idr at line 70 [8.31]

B:BD[10.116] → [10.116:173]

proofLTEThenLTESuccesor {x=Zero} ZeroLTEAny = ZeroLTEAny

[10.116]

[10.173]

proofLTEThenLTESuccesor ZeroLTEAny      = ZeroLTEAny

Replacement in src/Data/Natural.idr at line 86 [8.31]

B:BD[9.774] → [9.774:827]

      No cp => No $ proofNotLTEThenNotSuccesorLTE cp

[9.774]

[9.827]

      No cp => No  $ proofNotLTEThenNotSuccesorLTE cp

Replacement in src/Data/Natural.idr at line 106 [8.31]

B:BD[10.545] → [10.545:599]

       No cp => No $ proofNotLTEThenNotSuccesorLTE cp

[10.545]

[10.599]

       No cp => No  $ proofNotLTEThenNotSuccesorLTE cp

Replacement in src/Data/Natural.idr at line 118 [8.31]
B:BD[10.1108] → [10.1108:1145]
```
      Left l => Left $ SuccesorLTE l
```
[10.1108]
[10.1145]
```
      Left  l => Left  $ SuccesorLTE   l
```
Deletion in src/Data/Natural.idr at line 141 [8.31]
B:BD[5.86] → [5.86:94]
```
partial
```
Replacement in src/Data/Natural.idr at line 245 [8.31]
B:BD[11.1330] → [11.1330:1338]
```
partial
```
[11.1330]
[11.1338]
```
public export
```
Deletion in src/Data/LinkedList.idr at line 7 [12.17]
B:BD[12.58] → [13.752:787]
```
import Algebra.Control.Applicative
```
Insertion in src/Data/LinkedList.idr at line 8 [12.17]
[13.854]
[13.854]
```
import Algebra.Control.Applicative
```
Insertion in src/Data/LinkedList.idr at line 12 [12.17]
[14.511]
[13.883]
```
import Algebra.Group.Semigroup
```
Deletion in src/Data/LinkedList.idr at line 14 [12.17]
B:BD[13.911] → [14.512:543]
```
import Algebra.Group.Semigroup
```
Deletion in src/Data/LinkedList.idr at line 41 [12.17]
∅:D[15.584] → [12.921:963]
B:BD[12.921] → [12.921:963]
```
fromNotEquivHead ctr BothEmpty impossible
```
Deletion in src/Data/LinkedList.idr at line 46 [12.17]
∅:D[15.786] → [12.1126:1168]
B:BD[12.1126] → [12.1126:1168]
```
fromNotEquivTail ctr BothEmpty impossible
```

Replacement in src/Data/LinkedList.idr at line 49 [12.17]

B:BD[15.887] → [15.887:1087]

decLinkedListEquiv Nil Nil = Yes $ BothEmpty
decLinkedListEquiv Nil (_ :: _) = No $ absurd
decLinkedListEquiv (_ :: _) Nil = No $ absurd
decLinkedListEquiv @{e} (h1 :: t1) (h2 :: t2) = assert_total $

[15.887]

[15.1087]

decLinkedListEquiv Nil Nil = Yes BothEmpty
decLinkedListEquiv Nil (_::_) = No absurd
decLinkedListEquiv (_::_) Nil = No absurd
decLinkedListEquiv @{e} (h1::t1) (h2::t2) =

Replacement in src/Data/LinkedList.idr at line 94 [12.17]
B:BD[12.1758] → [12.1758:1808]
```
  map _ Nil = Nil
  map f (h::t) = f h :: map f t
```
[12.1758]
[12.1808]
```
  _ <$> Nil = Nil
  f <$> (h::t) = f h :: f <$> t
```

Replacement in src/Data/LinkedList.idr at line 98 [12.17]

B:BD[12.1836] → [12.1836:1935]

  proofIdentity (h::t) with (proofIdentity t)
    proofIdentity (h::t) | prf = rewrite prf in Refl

[12.1836]

[12.1935]

  proofIdentity (_::t) with (proofIdentity t)
    proofIdentity (_::_) | prf = rewrite prf in Refl

Replacement in src/Data/LinkedList.idr at line 101 [12.17]

B:BD[12.1936] → [12.1936:2041]

  proofComposition f g Nil = Refl
  proofComposition f g (h::t) = rewrite proofComposition f g t in Refl

[12.1936]

[16.28]

  proofComposition f g Nil    = Refl
  proofComposition f g (_::t) = rewrite proofComposition f g t in Refl

Replacement in src/Data/LinkedList.idr at line 107 [12.17]
B:BD[16.121] → [16.121:157]
```
app (f::fs) l = map f l <> app fs l
```
[16.121]
[16.157]
```
app (f::fs) l = (f <$> l) <> app fs l
```
Replacement in src/Data/LinkedList.idr at line 123 [12.17]
B:BD[16.493] → [16.493:538]
```
      rewrite concatNil (map identity xs) in
```
[16.493]
[16.538]
```
      rewrite concatNil (identity <$> xs) in
```
Replacement in src/Data/LinkedList.idr at line 134 [12.17]
B:BD[16.795] → [16.795:836]
```
    -- rewrite concatNil (map (.) gs) in
```
[16.795]
[16.836]
```
    -- rewrite concatNil ((.) <$> gs) in
```
Insertion in src/Data/LinkedList.idr at line 137 [12.17]
[16.892]
[16.892]
```
    -- rewrite concatNil ((.) <$> gs) in
```

Replacement in src/Data/Either.idr at line 16 [17.13]

B:BD[17.218] → [17.218:277]

  map f (Left x)  = Left x
  map f (Right x) = Right $ f x

[17.218]

[17.277]

  f <$> (Left  x) = Left x
  f <$> (Right x) = Right $ f x

Replacement in src/Data/Either.idr at line 19 [17.13]
B:BD[17.278] → [17.278:311]
```
  proofIdentity (Left _)  = Refl
```
[17.278]
[17.311]
```
  proofIdentity (Left  _) = Refl
```

Replacement in src/Data/Either.idr at line 29 [17.13]

B:BD[17.484] → [17.484:554]

  (Left x)  <*> _         = Left x
  (Right _) <*> (Left y)  = Left y

[17.484]

[17.554]

  (Left  x) <*> _         = Left x
  (Right _) <*> (Left  y) = Left y

Replacement in src/Data/Either.idr at line 41 [17.13]

B:BD[17.771] → [17.771:915]

  proofComposition (Left _)  (Left _)  _ = Refl
  proofComposition (Left _)  (Right _) _ = Refl
  proofComposition (Right _) (Left _)  _ = Refl

[17.771]

[17.915]

  proofComposition (Left  _) (Left  _) _ = Refl
  proofComposition (Left  _) (Right _) _ = Refl
  proofComposition (Right _) (Left  _) _ = Refl

Replacement in src/Data/Either.idr at line 45 [17.13]
B:BD[17.968] → [17.968:987]
```
    Left x => Refl
```
[17.968]
[17.987]
```
    Left  x => Refl
```
Replacement in src/Data/Either.idr at line 50 [17.13]
B:BD[17.1045] → [14.615:642]
```
  (Left x)  >>= _ = Left x
```
[17.1045]
[14.642]
```
  (Left  x) >>= _ = Left x
```

Replacement in src/Data/Boolean.idr at line 49 [7.117]

B:BD[7.214] → [18.688:845]

  decEquiv False False = Yes $ BothFalse
  decEquiv True  True  = Yes $ BothTrue
  decEquiv False True  = No  $ absurd
  decEquiv True  False = No  $ absurd

[7.214]

[19.212]

  decEquiv False False = Yes BothFalse
  decEquiv True  True  = Yes BothTrue
  decEquiv False True  = No  absurd
  decEquiv True  False = No  absurd

Replacement in src/Data/Boolean.idr at line 56 [7.117]
B:BD[19.297] → [19.297:334]
```
  TrueLTETrue : BooleanLTE True True
```
[19.297]
[19.334]
```
  TrueLTETrue : BooleanLTE True  True
```
Replacement in src/Data/Boolean.idr at line 68 [7.117]
B:BD[19.562] → [19.562:595]
```
  decLTE True  False = No absurd
```
[19.562]
[19.595]
```
  decLTE True  False = No  absurd
```
Replacement in src/Data/Boolean.idr at line 93 [7.117]
B:BD[19.1264] → [19.1264:1296]
```
  decLT False False = No absurd
```
[19.1264]
[19.1296]
```
  decLT False False = No  absurd
```
Replacement in src/Data/Boolean.idr at line 95 [7.117]
B:BD[19.1334] → [19.1334:1366]
```
  decLT True  _     = No absurd
```
[19.1334]
[19.1366]
```
  decLT True  _     = No  absurd
```
Replacement in src/Data/Boolean.idr at line 159 [7.117]
∅:D[3.182] → [20.912:956]
B:BD[20.912] → [20.912:956]
```
  proofLeftIdentity = proofDisjLeftIdentity
```
[3.182]
[20.956]
```
  proofLeftIdentity  = proofDisjLeftIdentity
```
Replacement in src/Data/Boolean.idr at line 202 [7.117]
B:BD[20.1520] → [20.1520:1552]
```
  proofAssociativity True b c =
```
[20.1520]
[20.1552]
```
  proofAssociativity True  b c =
```

Replacement in src/Data/Boolean.idr at line 241 [7.117]

B:BD[21.721] → [21.721:1049]

  proofGreatestLowerBound False False False FalseLTEAny FalseLTEAny = FalseLTEAny
  proofGreatestLowerBound False False True  FalseLTEAny FalseLTEAny = FalseLTEAny
  proofGreatestLowerBound False True  False FalseLTEAny FalseLTEAny = FalseLTEAny
  proofGreatestLowerBound False True  True  FalseLTEAny FalseLTEAny = FalseLTEAny

[21.721]

[21.1049]

  proofGreatestLowerBound False y     z     FalseLTEAny FalseLTEAny = FalseLTEAny

Replacement in src/Control/IO.idr at line 16 [22.2100]

B:BD[22.2379] → [22.2379:2443]

  map f (MkIO p) = MkIO (p `prim__io_bind` (prim__io_pure . f))

[22.2379]

[22.2443]

  f <$> (MkIO p) = MkIO (p `prim__io_bind` (prim__io_pure . f))

Replacement in src/Algebra/Relation/Order.idr at line 19 [23.12]

B:BD[23.430] → [19.27:112]

  proofLTEThenLTOrEquiv : (x, y : t) -> x `LTE` y -> Either (x `LT` y) (x `Equiv` y)

[23.430]

[4.66]

  proofLTEThenLTOrEquiv : (x, y : t) -> x `LTE` y
                        -> Either (x `LT` y) (x `Equiv` y)

Replacement in src/Algebra/Lattice/MeetSemilattice.idr at line 21 [24.581]

B:BD[24.1022] → [24.1022:1108]

  proofGreatestLowerBound : (b, x, y : t) -> b `LTE` x -> b `LTE` y -> b `LTE` x /\ y

[24.1022]

  proofGreatestLowerBound : (b, x, y : t) -> b `LTE` x -> b `LTE` y
                          -> b `LTE` x /\ y

Replacement in src/Algebra/Lattice/JoinSemilattice.idr at line 21 [24.33]

B:BD[24.474] → [24.474:558]

  proofLeastUpperBound : (b, x, y : t) -> x `LTE` b -> y `LTE` b ->  x \/ y `LTE` b

[24.474]

  proofLeastUpperBound : (b, x, y : t) -> x `LTE` b -> y `LTE` b
                       ->  x \/ y `LTE` b

Insertion in src/Algebra/Control/Functor.idr at line 6 [6.14]
[6.70]
[6.70]
```
infixl 9 <$>
```
Replacement in src/Algebra/Control/Functor.idr at line 11 [6.14]
B:BD[6.111] → [6.111:142]
```
  map : (a -> b) -> t a -> t b
```
[6.111]
[6.142]
```
  (<$>) : (a -> b) -> t a -> t b
```

Replacement in src/Algebra/Control/Functor.idr at line 13 [6.14]

B:BD[6.143] → [6.143:301]

  proofIdentity : (x : t a) -> map Builtin.identity x = x
  proofComposition : (f : a -> b) -> (g : b -> c) -> (x : t a) -> map (g . f) x = map g . map f $ x

[6.143]

  proofIdentity : (x : t a) -> Builtin.identity <$> x = x
  proofComposition : (f : a -> b) -> (g : b -> c) -> (x : t a)
                   -> (g . f) <$> x = (g <$>) . (f <$>) $ x

Replacement in src/Algebra/Control/Applicative.idr at line 18 [25.18]

B:BD[25.512] → [25.512:596]

  proofInterchange : (f : t (a -> b)) -> (x : a) -> f <*> pure x = pure ($ x) <*> f

[25.512]

[2.0]

  proofInterchange : (f : t (a -> b)) -> (x : a)
                   -> f <*> pure x = pure ($ x) <*> f

Refactor

Dependencies

In channels

Change contents

Replacement in src/Data/Optional.idr at line 48 [7.30]

Replacement in src/Data/Natural.idr at line 53 [8.31]

Replacement in src/Data/Natural.idr at line 60 [8.31]

Replacement in src/Data/Natural.idr at line 70 [8.31]

Replacement in src/Data/Natural.idr at line 86 [8.31]

Replacement in src/Data/Natural.idr at line 106 [8.31]

Replacement in src/Data/Natural.idr at line 118 [8.31]

Deletion in src/Data/Natural.idr at line 141 [8.31]

Replacement in src/Data/Natural.idr at line 245 [8.31]

Deletion in src/Data/LinkedList.idr at line 7 [12.17]

Insertion in src/Data/LinkedList.idr at line 8 [12.17]

Insertion in src/Data/LinkedList.idr at line 12 [12.17]

Deletion in src/Data/LinkedList.idr at line 14 [12.17]

Deletion in src/Data/LinkedList.idr at line 41 [12.17]

Deletion in src/Data/LinkedList.idr at line 46 [12.17]

Replacement in src/Data/LinkedList.idr at line 49 [12.17]

Replacement in src/Data/LinkedList.idr at line 94 [12.17]

Replacement in src/Data/LinkedList.idr at line 98 [12.17]

Replacement in src/Data/LinkedList.idr at line 101 [12.17]

Replacement in src/Data/LinkedList.idr at line 107 [12.17]

Replacement in src/Data/LinkedList.idr at line 123 [12.17]

Replacement in src/Data/LinkedList.idr at line 134 [12.17]

Insertion in src/Data/LinkedList.idr at line 137 [12.17]

Replacement in src/Data/Either.idr at line 16 [17.13]

Replacement in src/Data/Either.idr at line 19 [17.13]

Replacement in src/Data/Either.idr at line 29 [17.13]

Replacement in src/Data/Either.idr at line 41 [17.13]

Replacement in src/Data/Either.idr at line 45 [17.13]

Replacement in src/Data/Either.idr at line 50 [17.13]

Replacement in src/Data/Boolean.idr at line 49 [7.117]

Replacement in src/Data/Boolean.idr at line 56 [7.117]

Replacement in src/Data/Boolean.idr at line 68 [7.117]

Replacement in src/Data/Boolean.idr at line 93 [7.117]

Replacement in src/Data/Boolean.idr at line 95 [7.117]

Replacement in src/Data/Boolean.idr at line 159 [7.117]

Replacement in src/Data/Boolean.idr at line 202 [7.117]