fabian/veribase-idr2 - Change QL75BDYCNRAF2NPJP3MJHUPM6JRIGJQWK2OG2NWKBOVZUZ75CHOAC

Add Commutative Group Interfaces

Created by fabian on June 15, 2021

QL75BDYCNRAF2NPJP3MJHUPM6JRIGJQWK2OG2NWKBOVZUZ75CHOAC

Dependencies

In channels

main

Change contents

Deletion in src/Data/Boolean.idr at line 122 [3.117]
∅:D[2.94] → [3.393:394]
∅:D[4.250] → [3.393:394]
B:BD[3.393] → [3.393:394]
B:BD[3.394] → [4.251:265]
B:BD[4.265] → [2.95:148]
```
public export
[BooleanDisjMagma] Magma Boolean where
  (<>) = disj
```

Insertion in src/Data/Boolean.idr at line 142 [3.117]

[3.773]


export
proofDisjCommutative : (a, b : Boolean) -> a `disj` b = b `disj` a
proofDisjCommutative False b =
  rewrite proofDisjLeftIdentity b in
  rewrite proofDisjRightIdentity b in
  Refl
proofDisjCommutative True b = rewrite proofDisjRightAnnihilation b in Refl
public export
[BooleanDisjMagma] Magma Boolean where
  (<>) = disj

Insertion in src/Data/Boolean.idr at line 156 [3.117]

[4.578]

[BooleanDisjCommutativeMagma] CommutativeMagma Boolean using BooleanDisjMagma where
  proofCommutativity = proofDisjCommutative
public export

Insertion in src/Data/Boolean.idr at line 167 [3.117]

[4.816]

[3.904]


public export
[BooleanDisjCommutativeSemigroup] CommutativeSemigroup Boolean using BooleanDisjCommutativeMagma BooleanDisjSemigroup where

Replacement in src/Data/Boolean.idr at line 178 [3.117]

B:BD[3.1039] → [2.183:190]

∅:D[2.190] → [3.1039:1294]

B:BD[3.1039] → [3.1039:1294]

export
proofDisjCommutative : (a, b : Boolean) -> a `disj` b = b `disj` a
proofDisjCommutative False b =
  rewrite proofDisjLeftIdentity b in
  rewrite proofDisjRightIdentity b in
  Refl
proofDisjCommutative True b = rewrite proofDisjRightAnnihilation b in Refl

[3.1039]

[3.1294]

public export
[BooleanDisjCommutativeMonoid] CommutativeMonoid Boolean using BooleanDisjCommutativeSemigroup BooleanDisjMonoid where

Deletion in src/Data/Boolean.idr at line 185 [3.117]
∅:D[2.273] → [3.1549:1550]
∅:D[4.1101] → [3.1549:1550]
B:BD[3.1549] → [3.1549:1550]
B:BD[3.1550] → [5.234:248]
B:BD[5.248] → [2.274:327]
```
public export
[BooleanConjMagma] Magma Boolean where
  (<>) = conj
```

Insertion in src/Data/Boolean.idr at line 205 [3.117]

[3.1929]


export
proofConjCommutative : (a, b : Boolean) -> a `conj` b = b `conj` a
proofConjCommutative False b = rewrite proofConjRightAnnihilation b in Refl
proofConjCommutative True b =
  rewrite proofConjLeftIdentity b in
  rewrite proofConjRightIdentity b in
  Refl
public export
[BooleanConjMagma] Magma Boolean where
  (<>) = conj
public export
[BooleanConjCommutativeMagma] CommutativeMagma Boolean using BooleanConjMagma where
  proofCommutativity = proofConjCommutative

Deletion in src/Data/Boolean.idr at line 237 [3.117]

B:BD[3.2193] → [2.362:369]

∅:D[2.369] → [3.2193:2441]

B:BD[3.2193] → [3.2193:2441]

B:BD[3.2696] → [3.2696:2703]

B:BD[3.2703] → [5.249:250]

export
proofConjCommutative : (a, b : Boolean) -> a `conj` b = b `conj` a
proofConjCommutative False b = rewrite proofConjRightAnnihilation b in Refl
proofConjCommutative True b =
  rewrite proofConjLeftIdentity b in
  rewrite proofConjRightIdentity b in
  Refl

Insertion in src/Algebra/Group/Semigroup.idr at line 12 [6.639]

[6.834]


public export
interface (CommutativeMagma t, Semigroup t) => CommutativeSemigroup t where
public export
CommutativeMagma t => Semigroup t => CommutativeSemigroup t where

Insertion in src/Algebra/Group/Monoid.idr at line 15 [6.395]

[6.622]


public export
interface (CommutativeSemigroup t, Monoid t) => CommutativeMonoid t where
CommutativeSemigroup t => Monoid t => CommutativeMonoid t where

Insertion in src/Algebra/Group/Magma.idr at line 12 [6.270]

[6.381]


public export
interface Magma t => CommutativeMagma t where
  proofCommutativity : (x, y : t) -> x <> y = y <> x

Insertion in src/Algebra/Group/Group.idr at line 16 [6.12]

[6.257]


public export
interface (CommutativeMonoid t, Group t) => CommutativeGroup t where
public export
CommutativeMonoid t => Group t => CommutativeGroup t where