fabian/veribase-idr2 - Change WGQEJYGCJTGLKYTOBJNBPIOBFLQMO7XDVRSK7VFNG6GKE7FGAELAC

Refactor

Created by fabian on June 11, 2021

WGQEJYGCJTGLKYTOBJNBPIOBFLQMO7XDVRSK7VFNG6GKE7FGAELAC

Dependencies

In channels

main

Change contents

Deletion in src/Data/Optional.idr at line 5 [4.30]
B:BD[4.53] → [5.912:947]
```
import Algebra.Control.Applicative
```
Insertion in src/Data/Optional.idr at line 6 [4.30]
[5.983]
[5.983]
Insertion in src/Data/Optional.idr at line 8 [4.30]
[5.1014]
[5.1014]
```
import Algebra.Control.Applicative
```

Replacement in src/Data/Optional.idr at line 22 [4.30]

B:BD[6.1211] → [7.1655:1734]

(e : Equivalence t) => Uninhabited (OptionalEquiv @{e} Nothing (Some b)) where

[6.1211]

[6.1262]

(e : Equivalence t) =>
Uninhabited (OptionalEquiv @{e} Nothing (Some b)) where

Replacement in src/Data/Optional.idr at line 28 [4.30]

B:BD[6.1353] → [7.1735:1814]

(e : Equivalence t) => Uninhabited (OptionalEquiv @{e} (Some a) Nothing) where

[6.1353]

[6.1404]

(e : Equivalence t) =>
Uninhabited (OptionalEquiv @{e} (Some a) Nothing) where

Replacement in src/Data/Optional.idr at line 34 [4.30]

B:BD[6.1495] → [6.1495:1644]

fromNotEquiv : Equivalence t => {a, b : t} -> (ok : Not (Equiv a b)) -> Not (OptionalEquiv (Some a) (Some b))
fromNotEquiv ok BothNothing impossible

[6.1495]

[7.1815]

fromNotEquiv : Equivalence t => {a, b : t} -> Not (Equiv a b)
             -> Not (OptionalEquiv (Some a) (Some b))

Replacement in src/Data/Optional.idr at line 42 [4.30]

B:BD[6.1771] → [6.1771:1906]

  decEquiv Nothing  Nothing  = Yes $ BothNothing
  decEquiv Nothing  (Some _) = No $ absurd
  decEquiv (Some _) Nothing  = No $ absurd

[6.1771]

[2.0]

  decEquiv Nothing  Nothing  = Yes BothNothing
  decEquiv Nothing  (Some _) = No  absurd
  decEquiv (Some _) Nothing  = No  absurd

Replacement in src/Data/Optional.idr at line 47 [4.30]
B:BD[2.90] → [2.90:130]
```
    (No ctra) => No $ fromNotEquiv ctra
```
[2.90]
[8.342]
```
    (No ctra) => No  $ fromNotEquiv ctra
```
Replacement in src/Data/Optional.idr at line 51 [4.30]
B:BD[8.380] → [3.0:27]
```
  f <$>  Nothing = Nothing
```
[8.380]
[3.27]
```
  _ <$>  Nothing = Nothing
```
Replacement in src/Data/Optional.idr at line 55 [4.30]
B:BD[8.472] → [8.472:504]
```
  proofIdentity (Some a) = Refl
```
[8.472]
[8.504]
```
  proofIdentity (Some _) = Refl
```

Replacement in src/Data/Optional.idr at line 57 [4.30]

B:BD[8.505] → [8.505:583]

  proofComposition f g Nothing  = Refl
  proofComposition f g (Some a) = Refl

[8.505]

[9.28]

  proofComposition _ _ Nothing  = Refl
  proofComposition _ _ (Some _) = Refl

Replacement in src/Data/Optional.idr at line 69 [4.30]
B:BD[9.207] → [9.207:239]
```
  proofIdentity (Some x) = Refl
```
[9.207]
[9.239]
```
  proofIdentity (Some _) = Refl
```

Replacement in src/Data/Optional.idr at line 72 [4.30]

B:BD[9.286] → [9.286:484]

  proofComposition Nothing  (Some g) _ = Refl
  proofComposition (Some f) Nothing  _ = Refl
  proofComposition (Some f) (Some g) Nothing  = Refl
  proofComposition (Some f) (Some g) (Some x) = Refl

[9.286]

[9.484]

  proofComposition Nothing  (Some _) _ = Refl
  proofComposition (Some _) Nothing  _ = Refl
  proofComposition (Some _) (Some _) z = case z of
    Nothing  => Refl
    (Some _) => Refl

Replacement in src/Data/Optional.idr at line 78 [4.30]
B:BD[9.485] → [9.485:516]
```
  proofHomomorphism f x = Refl
```
[9.485]
[9.516]
```
  proofHomomorphism _ _ = Refl
```

Replacement in src/Data/Optional.idr at line 80 [4.30]

B:BD[9.517] → [9.517:591]

  proofInterchange Nothing  x = Refl
  proofInterchange (Some f) x = Refl

[9.517]

[10.22]

  proofInterchange Nothing  _ = Refl
  proofInterchange (Some _) _ = Refl

Replacement in src/Data/Optional.idr at line 85 [4.30]
B:BD[10.58] → [11.395:421]
```
  Nothing >>= _ = Nothing
```
[10.58]
[11.421]
```
  Nothing >>=  _ = Nothing
```
Replacement in src/Data/Optional.idr at line 88 [4.30]
B:BD[10.111] → [10.111:142]
```
  proofLeftIdentity x f = Refl
```
[10.111]
[10.142]
```
  proofLeftIdentity _ _ = Refl
```
Replacement in src/Data/Optional.idr at line 91 [4.30]
B:BD[10.180] → [10.180:217]
```
  proofRightIdentity (Some x) = Refl
```
[10.180]
[10.217]
```
  proofRightIdentity (Some _) = Refl
```

Replacement in src/Data/Optional.idr at line 93 [4.30]

B:BD[10.218] → [10.218:300]

  proofAssociativity Nothing  f g = Refl
  proofAssociativity (Some x) f g = Refl

[10.218]

  proofAssociativity Nothing  _ _ = Refl
  proofAssociativity (Some _) _ _ = Refl

Refactor

Dependencies

In channels

Change contents

Deletion in src/Data/Optional.idr at line 5 [4.30]

Insertion in src/Data/Optional.idr at line 6 [4.30]

Insertion in src/Data/Optional.idr at line 8 [4.30]

Replacement in src/Data/Optional.idr at line 22 [4.30]

Replacement in src/Data/Optional.idr at line 28 [4.30]

Replacement in src/Data/Optional.idr at line 34 [4.30]

Replacement in src/Data/Optional.idr at line 42 [4.30]

Replacement in src/Data/Optional.idr at line 47 [4.30]

Replacement in src/Data/Optional.idr at line 51 [4.30]

Replacement in src/Data/Optional.idr at line 55 [4.30]

Replacement in src/Data/Optional.idr at line 57 [4.30]

Replacement in src/Data/Optional.idr at line 69 [4.30]

Replacement in src/Data/Optional.idr at line 72 [4.30]

Replacement in src/Data/Optional.idr at line 78 [4.30]

Replacement in src/Data/Optional.idr at line 80 [4.30]

Replacement in src/Data/Optional.idr at line 85 [4.30]

Replacement in src/Data/Optional.idr at line 88 [4.30]

Replacement in src/Data/Optional.idr at line 91 [4.30]

Replacement in src/Data/Optional.idr at line 93 [4.30]