fabian/veribase-idr2 - Change 3WLOPTAUKTLZP3B3DY6J7AKA4AKYGW34MGZRLWCKKR2Q6GUQTUPQC

Refactor

Created by fabian on June 11, 2021

3WLOPTAUKTLZP3B3DY6J7AKA4AKYGW34MGZRLWCKKR2Q6GUQTUPQC

Dependencies

In channels

main

Change contents

Replacement in src/Data/Natural.idr at line 68 [4.31]
B:BD[3.32] → [3.32:46]
```
public export
```
[3.32]
[3.46]
```
export
```
Replacement in src/Data/Natural.idr at line 73 [4.31]
B:BD[5.376] → [5.376:390]
```
public export
```
[5.376]
[5.390]
```
export
```

Replacement in src/Data/Natural.idr at line 91 [4.31]

B:BD[5.933] → [5.933:1115]

  proofTransitivity Zero        Zero            z  ZeroLTEAny  ZeroLTEAny     = ZeroLTEAny
  proofTransitivity Zero (Succesor y) (Succesor z) ZeroLTEAny (SuccesorLTE p) = ZeroLTEAny

[5.933]

[5.1115]

  proofTransitivity Zero Zero _ ZeroLTEAny ZeroLTEAny = ZeroLTEAny
  proofTransitivity Zero (Succesor _) (Succesor _) ZeroLTEAny (SuccesorLTE _) = ZeroLTEAny

Replacement in src/Data/Natural.idr at line 101 [4.31]

B:BD[3.355] → [3.355:412]

  decLT Zero (Succesor y) = Yes $ SuccesorLTE ZeroLTEAny

[3.355]

[3.412]

  decLT Zero (Succesor _) = Yes $ SuccesorLTE ZeroLTEAny

Replacement in src/Data/Natural.idr at line 115 [4.31]

B:BD[3.915] → [3.915:1000]

  proofLTEThenLTOrEquiv Zero (Succesor y) ZeroLTEAny = Left $ SuccesorLTE ZeroLTEAny

[3.915]

[3.1000]

  proofLTEThenLTOrEquiv Zero (Succesor _) ZeroLTEAny = Left $ SuccesorLTE ZeroLTEAny

Replacement in src/Data/Natural.idr at line 136 [4.31]

B:BD[6.8] → [6.8:95]

proofPlusLeftReduction : (x, y : Natural) -> plus (Succesor x) y = Succesor (plus x y)

[6.8]

[6.95]

proofPlusLeftReduction : (x, y : Natural)
                       -> plus (Succesor x) y = Succesor (plus x y)

Replacement in src/Data/Natural.idr at line 151 [4.31]

B:BD[2.365] → [2.365:486]

proofPlusAssociative : (x, y, z : Natural) -> plus x (plus y z) = plus (plus x y) z
proofPlusAssociative x y Zero = Refl

[2.365]

[2.486]

proofPlusAssociative : (x, y, z : Natural)
                     -> plus x (plus y z) = plus (plus x y) z
proofPlusAssociative _ _ Zero = Refl

Replacement in src/Data/Natural.idr at line 170 [4.31]
B:BD[7.810] → [7.810:840]
```
  proofRightIdentity x = Refl
```
[7.810]
[6.331]
```
  proofRightIdentity _ = Refl
```
Replacement in src/Data/Natural.idr at line 188 [4.31]
B:BD[6.825] → [6.825:867]
```
  rewrite proofPlusLeftIdentity x in Refl
```
[6.825]
[6.867]
```
  rewrite proofPlusLeftIdentity x in
  Refl
```

Replacement in src/Data/Natural.idr at line 194 [4.31]

B:BD[6.977] → [6.977:1062]

proofMultLeftAnnihilation (Succesor x) = rewrite proofMultLeftAnnihilation x in Refl

[6.977]

[6.1062]

proofMultLeftAnnihilation (Succesor x) =
  rewrite proofMultLeftAnnihilation x in Refl

Replacement in src/Data/Natural.idr at line 200 [4.31]

B:BD[6.1174] → [6.1174:1261]

proofMultRightAnnihilation (Succesor x) = rewrite proofMultRightAnnihilation x in Refl

[6.1174]

[2.617]

proofMultRightAnnihilation (Succesor x) =
  rewrite proofMultRightAnnihilation x in Refl

Replacement in src/Data/Natural.idr at line 206 [4.31]

B:BD[2.726] → [2.726:896]

proofMultCommutative Zero (Succesor y) = rewrite proofMultCommutative Zero y in Refl
proofMultCommutative (Succesor x) Zero = rewrite proofMultCommutative Zero x in Refl

[2.726]

[2.896]

proofMultCommutative Zero (Succesor y) =
  rewrite proofMultCommutative Zero y in Refl
proofMultCommutative (Succesor x) Zero =
  rewrite proofMultCommutative Zero x in Refl

Replacement in src/Data/Natural.idr at line 222 [4.31]

B:BD[2.1360] → [2.1360:1445]

proofMultLeftReduction : (x, y : Natural) -> mult (Succesor x) y = plus y (mult x y)

[2.1352]

[2.1445]

proofMultLeftReduction : (x, y : Natural)
                       -> mult (Succesor x) y = plus y (mult x y)

Replacement in src/Data/Natural.idr at line 230 [4.31]

B:BD[2.1584] → [2.1584:1685]

proofMultLeftDistributesPlus : (x, y, z : Natural) -> mult x (plus y z) = plus (mult x y) (mult x z)

[2.1576]

[2.1685]

proofMultLeftDistributesPlus : (x, y, z : Natural)
                             -> mult x (plus y z) = plus (mult x y) (mult x z)