Skip to content

Latest commit

 

History

History
135 lines (113 loc) · 5.76 KB

CHANGELOG.md

File metadata and controls

135 lines (113 loc) · 5.76 KB

Version 2.3-dev

The library has been tested using Agda 2.7.0 and 2.7.0.1.

Highlights

Bug-fixes

Non-backwards compatible changes

  • The implementation of ≤-total in Data.Nat.Properties has been altered to use operations backed by primitives, rather than recursion, making it significantly faster. However, its reduction behaviour on open terms may have changed.

  • issue #2471 In Relation.Binary.Definitions, the left/right order of the components of _Respects₂_ have been swapped. Previously the position of the _Respectsˡ_ (respects left) component was placed on the right hand side of the pair and _Respectsʳ_ (respects right) was placed on the left hand side of the pair. By switching them the names are now consistent with their location.

Minor improvements

Deprecated modules

Deprecated names

  • In Algebra.Definitions.RawMagma:

    _∣∣_   ↦  _∥_
_∤∤_    ↦  _∦_

  • In `Algebra.Module.Consequences

    *ₗ-assoc+comm⇒*ᵣ-assoc      ↦  *ₗ-assoc∧comm⇒*ᵣ-assoc
*ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
*ᵣ-assoc+comm⇒*ₗ-assoc      ↦  *ᵣ-assoc∧comm⇒*ₗ-assoc
*ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc

  • In Algebra.Properties.Magma.Divisibility:

    ∣∣-sym       ↦  ∥-sym
∣∣-respˡ-≈   ↦  ∥-respˡ-≈
∣∣-respʳ-≈   ↦  ∥-respʳ-≈
∣∣-resp-≈    ↦  ∥-resp-≈
∤∤-sym  -≈    ↦  ∦-sym
∤∤-respˡ-≈    ↦  ∦-respˡ-≈
∤∤-respʳ-≈    ↦  ∦-respʳ-≈
∤∤-resp-≈     ↦  ∦-resp-≈

  • In Algebra.Properties.Monoid.Divisibility:

    ∣∣-refl            ↦  ∥-refl
∣∣-reflexive       ↦  ∥-reflexive
∣∣-isEquivalence   ↦  ∥-isEquivalence

  • In Algebra.Properties.Semigroup.Divisibility:

    ∣∣-trans   ↦  ∥-trans

  • In Data.List.Base:

    and       ↦  Data.Bool.ListAction.and
or        ↦  Data.Bool.ListAction.or
any       ↦  Data.Bool.ListAction.any
all       ↦  Data.Bool.ListAction.all
sum       ↦  Data.Nat.ListAction.sum
product   ↦  Data.Nat.ListAction.product

  • In Data.List.Properties:

    sum-++       ↦  Data.Nat.ListAction.Properties.sum-++
∈⇒∣product   ↦  Data.Nat.ListAction.Properties.∈⇒∣product
product≢0    ↦  Data.Nat.ListAction.Properties.product≢0
∈⇒≤product   ↦  Data.Nat.ListAction.Properties.∈⇒≤product

  • In Data.List.Relation.Binary.Permutation.Propositional.Properties:

    sum-↭       ↦  Data.Nat.ListAction.Properties.sum-↭
product-↭   ↦  Data.Nat.ListAction.Properties.product-↭

New modules

  • Data.List.Base.{and|or|any|all} have been lifted out into Data.Bool.ListAction.

  • Data.List.Base.{sum|product} and their properties have been lifted out into Data.Nat.ListAction and Data.Nat.ListAction.Properties.

Additions to existing modules

  • In Algebra.Construct.Pointwise: 
    isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →
                                  IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isSemiringWithoutOne            : IsSemiringWithoutOne _≈_ _+_ _*_ 0# →
                                  IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# →
                                  IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiring           : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# →
                                  IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isIdempotentSemiring            : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# →
                                  IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isKleeneAlgebra                 : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# →
                                  IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#)
isQuasiring                     : IsQuasiring _≈_ _+_ _*_ 0# 1# →
                                  IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isCommutativeRing               : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# →
                                  IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
commutativeMonoid               : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ)
nearSemiring                    : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)
semiringWithoutOne              : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiringWithoutOne   : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiring             : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ)
idempotentSemiring              : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ)
kleeneAlgebra                   : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ)
quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)