File tree Expand file tree Collapse file tree 1 file changed +5
-5
lines changed Expand file tree Collapse file tree 1 file changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -53,7 +53,7 @@ Deprecated names
53
53
∣-respˡ ↦ ∣-respˡ-≈
54
54
∣-respʳ ↦ ∣-respʳ-≈
55
55
∣-resp ↦ ∣-resp-≈
56
- ```
56
+ ```
57
57
58
58
* In ` Algebra.Solver.CommutativeMonoid ` :
59
59
``` agda
@@ -293,12 +293,12 @@ Additions to existing modules
293
293
``` agda
294
294
Env : ℕ → Set _
295
295
Env = Vec Carrier
296
- ```
296
+ ```
297
297
298
298
* In ` Algebra.Structures.RingWithoutOne ` :
299
299
``` agda
300
300
isNearSemiring : IsNearSemiring _ _
301
- ```
301
+ ```
302
302
303
303
* In ` Data.List.Membership.Propositional.Properties ` :
304
304
``` agda
@@ -544,7 +544,7 @@ Additions to existing modules
544
544
``` agda
545
545
value-injective : value v ≡ value w → v ≡ w
546
546
_≟_ : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ]
547
- ```
547
+ ```
548
548
549
549
* New lemma in ` Data.Vec.Properties ` :
550
550
``` agda
@@ -570,7 +570,7 @@ Additions to existing modules
570
570
×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
571
571
×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
572
572
∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
573
- ```
573
+ ```
574
574
575
575
* In ` Relation.Binary.Bundles ` :
576
576
``` agda
You can’t perform that action at this time.
0 commit comments