fabian/veribase-idr2 - Change WJJ6PMS6GYR5NIQI6Q6YH6WQSTJ3U56F3KZJOSYHTRAZ5MKIPXAAC

Refactor

Created by fabian on June 11, 2021

WJJ6PMS6GYR5NIQI6Q6YH6WQSTJ3U56F3KZJOSYHTRAZ5MKIPXAAC

Dependencies

In channels

main

Change contents

Replacement in src/Data/Natural.idr at line 130 [3.31]
B:BD[2.218] → [2.218:232]
```
public export
```
[2.218]
[2.232]
```
export
```

Replacement in src/Data/Boolean.idr at line 119 [5.117]

B:BD[4.162] → [4.162:250]

[BooleanDisjMagma] Magma Boolean where
  False <> False = False
  _     <> _     = True

[4.162]

[5.393]

disj : Boolean -> Boolean -> Boolean
disj False False = False
disj _     _     = True

Replacement in src/Data/Boolean.idr at line 124 [5.117]
∅:D[4.265] → [5.394:431]
B:BD[5.394] → [5.394:431]
B:BD[5.431] → [4.266:298]
```
disj : Boolean -> Boolean -> Boolean
disj = (<>) @{BooleanDisjMagma}
```
[4.265]
[4.298]
```
[BooleanDisjMagma] Magma Boolean where
  (<>) = disj
```
Insertion in src/Data/Boolean.idr at line 127 [5.117]
[4.299]
[4.299]
```
export
```
Insertion in src/Data/Boolean.idr at line 132 [5.117]
[4.430]
[4.430]
```
export
```
Insertion in src/Data/Boolean.idr at line 137 [5.117]
[5.481]
[5.481]
```
export
```
Insertion in src/Data/Boolean.idr at line 142 [5.117]
[5.626]
[5.626]
```
export
```
Insertion in src/Data/Boolean.idr at line 158 [5.117]
[4.912]
[4.912]
Insertion in src/Data/Boolean.idr at line 162 [5.117]
[5.1039]
[5.1039]
```
export
```

Replacement in src/Data/Boolean.idr at line 171 [5.117]

B:BD[4.1017] → [4.1017:1101]

[BooleanConjMagma] Magma Boolean where
  True <> True = True
  _    <> _    = False

[4.1017]

[5.1549]

conj : Boolean -> Boolean -> Boolean
conj True True = True
conj _    _    = False

Replacement in src/Data/Boolean.idr at line 176 [5.117]
∅:D[6.248] → [5.1550:1587]
B:BD[5.1550] → [5.1550:1587]
B:BD[5.1587] → [4.1102:1134]
```
conj : Boolean -> Boolean -> Boolean
conj = (<>) @{BooleanConjMagma}
```
[6.248]
[4.1134]
```
[BooleanConjMagma] Magma Boolean where
  (<>) = conj
```
Insertion in src/Data/Boolean.idr at line 179 [5.117]
[4.1135]
[4.1135]
```
export
```
Insertion in src/Data/Boolean.idr at line 184 [5.117]
[4.1265]
[4.1265]
```
export
```
Insertion in src/Data/Boolean.idr at line 189 [5.117]
[5.1633]
[5.1633]
```
export
```
Insertion in src/Data/Boolean.idr at line 194 [5.117]
[5.1780]
[5.1780]
```
export
```
Insertion in src/Data/Boolean.idr at line 210 [5.117]
[4.1745]
[4.1745]
Insertion in src/Data/Boolean.idr at line 214 [5.117]
[5.2193]
[5.2193]
```
export
```
Insertion in src/Data/Boolean.idr at line 232 [5.117]
[6.377]
[6.377]
Insertion in src/Data/Boolean.idr at line 253 [5.117]
[6.1255]
[6.1255]