[Git][haskell-team/agda-stdlib][upstream] New upstream version 2.3
Ilias Tsitsimpis (@iliastsi)
gitlab at salsa.debian.org
Sun Feb 15 14:12:04 GMT 2026
Ilias Tsitsimpis pushed to branch upstream at Debian Haskell Group / agda-stdlib
Commits:
d297d2d9 by Ilias Tsitsimpis at 2026-02-15T14:56:59+02:00
New upstream version 2.3
- - - - -
703 changed files:
- .github/workflows/ci-ubuntu.yml
- .github/workflows/haskell-ci.yml
- CHANGELOG.md
- CHANGELOG/v1.3.md
- + CHANGELOG/v2.1.1.md
- + CHANGELOG/v2.1.md
- + CHANGELOG/v2.2.md
- CITATION.cff
- LICENCE
- agda-stdlib-utils.cabal
- doc/README.agda
- doc/README/Data/List.agda
- doc/README/Data/Tree/AVL.agda
- doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
- doc/README/Design/Hierarchies.agda
- doc/installation-guide.md
- doc/release-guide.txt
- doc/style-guide.md
- src/Algebra/Apartness/Bundles.agda
- src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
- src/Algebra/Apartness/Structures.agda
- src/Algebra/Bundles.agda
- src/Algebra/Bundles/Raw.agda
- src/Algebra/Consequences/Base.agda
- src/Algebra/Consequences/Propositional.agda
- src/Algebra/Consequences/Setoid.agda
- src/Algebra/Construct/Add/Identity.agda
- src/Algebra/Construct/Flip/Op.agda
- src/Algebra/Construct/Initial.agda
- src/Algebra/Construct/LiftedChoice.agda
- src/Algebra/Construct/NaturalChoice/Base.agda
- src/Algebra/Construct/NaturalChoice/Max.agda
- src/Algebra/Construct/NaturalChoice/MaxOp.agda
- src/Algebra/Construct/NaturalChoice/Min.agda
- src/Algebra/Construct/NaturalChoice/MinMaxOp.agda
- src/Algebra/Construct/NaturalChoice/MinOp.agda
- src/Algebra/Construct/Pointwise.agda
- src/Algebra/Construct/Subst/Equality.agda
- src/Algebra/Construct/Terminal.agda
- src/Algebra/Construct/Zero.agda
- src/Algebra/Definitions.agda
- src/Algebra/Definitions/RawMagma.agda
- src/Algebra/Definitions/RawMonoid.agda
- src/Algebra/Definitions/RawSemiring.agda
- src/Algebra/Lattice/Bundles.agda
- src/Algebra/Lattice/Bundles/Raw.agda
- src/Algebra/Lattice/Construct/DirectProduct.agda
- src/Algebra/Lattice/Construct/LiftedChoice.agda
- src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda
- src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda
- src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda
- src/Algebra/Lattice/Construct/Subst/Equality.agda
- src/Algebra/Lattice/Construct/Zero.agda
- src/Algebra/Lattice/Morphism/Construct/Composition.agda
- src/Algebra/Lattice/Morphism/Construct/Identity.agda
- src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda
- src/Algebra/Lattice/Morphism/Structures.agda
- src/Algebra/Lattice/Properties/BooleanAlgebra.agda
- src/Algebra/Lattice/Properties/DistributiveLattice.agda
- src/Algebra/Lattice/Properties/Lattice.agda
- src/Algebra/Lattice/Properties/Semilattice.agda
- src/Algebra/Lattice/Structures.agda
- src/Algebra/Lattice/Structures/Biased.agda
- src/Algebra/Module/Bundles.agda
- src/Algebra/Module/Bundles/Raw.agda
- src/Algebra/Module/Consequences.agda
- src/Algebra/Module/Construct/DirectProduct.agda
- src/Algebra/Module/Construct/Idealization.agda
- src/Algebra/Module/Construct/TensorUnit.agda
- src/Algebra/Module/Construct/Zero.agda
- src/Algebra/Module/Definitions/Bi.agda
- src/Algebra/Module/Definitions/Bi/Simultaneous.agda
- src/Algebra/Module/Definitions/Left.agda
- src/Algebra/Module/Definitions/Right.agda
- + src/Algebra/Module/Morphism/BimoduleMonomorphism.agda
- + src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda
- src/Algebra/Module/Morphism/Construct/Composition.agda
- src/Algebra/Module/Morphism/Construct/Identity.agda
- src/Algebra/Module/Morphism/Definitions.agda
- + src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda
- + src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda
- src/Algebra/Module/Morphism/ModuleHomomorphism.agda
- + src/Algebra/Module/Morphism/ModuleMonomorphism.agda
- + src/Algebra/Module/Morphism/RightModuleMonomorphism.agda
- + src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda
- + src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda
- src/Algebra/Module/Morphism/Structures.agda
- src/Algebra/Module/Properties.agda
- + src/Algebra/Module/Properties/Bimodule.agda
- + src/Algebra/Module/Properties/LeftModule.agda
- + src/Algebra/Module/Properties/RightModule.agda
- src/Algebra/Module/Properties/Semimodule.agda
- src/Algebra/Module/Structures.agda
- src/Algebra/Module/Structures/Biased.agda
- src/Algebra/Morphism.agda
- + src/Algebra/Morphism/Bundles.agda
- src/Algebra/Morphism/Consequences.agda
- src/Algebra/Morphism/Construct/Composition.agda
- + src/Algebra/Morphism/Construct/DirectProduct.agda
- src/Algebra/Morphism/Construct/Identity.agda
- src/Algebra/Morphism/Construct/Initial.agda
- src/Algebra/Morphism/Construct/Terminal.agda
- src/Algebra/Morphism/GroupMonomorphism.agda
- src/Algebra/Morphism/MagmaMonomorphism.agda
- src/Algebra/Morphism/MonoidMonomorphism.agda
- src/Algebra/Morphism/RingMonomorphism.agda
- src/Algebra/Morphism/Structures.agda
- src/Algebra/Operations/Semiring.agda
- src/Algebra/Properties/AbelianGroup.agda
- src/Algebra/Properties/BooleanAlgebra.agda
- src/Algebra/Properties/BooleanAlgebra/Expression.agda
- src/Algebra/Properties/CancellativeCommutativeSemiring.agda
- src/Algebra/Properties/CommutativeMagma/Divisibility.agda
- src/Algebra/Properties/CommutativeMonoid.agda
- src/Algebra/Properties/CommutativeMonoid/Sum.agda
- src/Algebra/Properties/CommutativeSemigroup.agda
- src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda
- src/Algebra/Properties/CommutativeSemiring/Binomial.agda
- src/Algebra/Properties/CommutativeSemiring/Exp.agda
- src/Algebra/Properties/CommutativeSemiring/Exp/TCOptimised.agda
- src/Algebra/Properties/DistributiveLattice.agda
- src/Algebra/Properties/Group.agda
- + src/Algebra/Properties/IdempotentCommutativeMonoid.agda
- src/Algebra/Properties/KleeneAlgebra.agda
- src/Algebra/Properties/Loop.agda
- src/Algebra/Properties/Magma/Divisibility.agda
- + src/Algebra/Properties/Monoid.agda
- src/Algebra/Properties/Monoid/Divisibility.agda
- src/Algebra/Properties/Quasigroup.agda
- src/Algebra/Properties/RingWithoutOne.agda
- src/Algebra/Properties/Semigroup.agda
- src/Algebra/Properties/Semigroup/Divisibility.agda
- src/Algebra/Properties/Semiring/Binomial.agda
- src/Algebra/Properties/Semiring/Divisibility.agda
- src/Algebra/Properties/Semiring/Exp.agda
- src/Algebra/Properties/Semiring/Exp/TCOptimised.agda
- src/Algebra/Properties/Semiring/Exp/TailRecursiveOptimised.agda
- src/Algebra/Properties/Semiring/Mult.agda
- src/Algebra/Properties/Semiring/Primality.agda
- src/Algebra/Properties/Semiring/Sum.agda
- src/Algebra/Solver/CommutativeMonoid.agda
- + src/Algebra/Solver/CommutativeMonoid/Normal.agda
- src/Algebra/Solver/IdempotentCommutativeMonoid.agda
- src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda
- + src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda
- src/Algebra/Solver/Monoid.agda
- + src/Algebra/Solver/Monoid/Expression.agda
- + src/Algebra/Solver/Monoid/Normal.agda
- + src/Algebra/Solver/Monoid/Solver.agda
- src/Algebra/Solver/Ring.agda
- src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
- src/Algebra/Solver/Ring/Lemmas.agda
- src/Algebra/Solver/Ring/NaturalCoefficients.agda
- src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
- src/Algebra/Solver/Ring/Simple.agda
- src/Algebra/Structures.agda
- src/Axiom/DoubleNegationElimination.agda
- src/Axiom/ExcludedMiddle.agda
- src/Axiom/Extensionality/Heterogeneous.agda
- src/Axiom/Extensionality/Propositional.agda
- src/Axiom/UniquenessOfIdentityProofs.agda
- src/Axiom/UniquenessOfIdentityProofs/WithK.agda
- src/Codata/Guarded/M.agda
- src/Codata/Guarded/Stream.agda
- src/Codata/Guarded/Stream/Properties.agda
- src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
- src/Codata/Guarded/Stream/Relation/Unary/All.agda
- src/Codata/Guarded/Stream/Relation/Unary/Any.agda
- src/Codata/Musical/Cofin.agda
- src/Codata/Musical/Colist.agda
- src/Codata/Musical/Colist/Base.agda
- src/Codata/Musical/Colist/Bisimilarity.agda
- src/Codata/Musical/Colist/Infinite-merge.agda
- src/Codata/Musical/Colist/Properties.agda
- src/Codata/Musical/Colist/Relation/Unary/All/Properties.agda
- src/Codata/Musical/Colist/Relation/Unary/Any.agda
- src/Codata/Musical/Conat.agda
- src/Codata/Musical/Conat/Base.agda
- src/Codata/Musical/Covec.agda
- src/Codata/Musical/M.agda
- src/Codata/Musical/M/Indexed.agda
- src/Codata/Sized/Cofin/Literals.agda
- src/Codata/Sized/Colist.agda
- src/Codata/Sized/Colist/Bisimilarity.agda
- src/Codata/Sized/Colist/Effectful.agda
- src/Codata/Sized/Colist/Properties.agda
- src/Codata/Sized/Conat.agda
- src/Codata/Sized/Conat/Bisimilarity.agda
- src/Codata/Sized/Conat/Properties.agda
- src/Codata/Sized/Covec.agda
- src/Codata/Sized/Covec/Bisimilarity.agda
- src/Codata/Sized/Covec/Effectful.agda
- src/Codata/Sized/Covec/Instances.agda
- src/Codata/Sized/Covec/Properties.agda
- src/Codata/Sized/Cowriter.agda
- src/Codata/Sized/Cowriter/Bisimilarity.agda
- src/Codata/Sized/Delay.agda
- src/Codata/Sized/Delay/Bisimilarity.agda
- src/Codata/Sized/Delay/Effectful.agda
- src/Codata/Sized/Delay/Properties.agda
- src/Codata/Sized/M.agda
- src/Codata/Sized/M/Bisimilarity.agda
- src/Codata/Sized/M/Properties.agda
- src/Codata/Sized/Stream.agda
- src/Codata/Sized/Stream/Bisimilarity.agda
- src/Codata/Sized/Stream/Effectful.agda
- src/Codata/Sized/Stream/Instances.agda
- src/Codata/Sized/Stream/Properties.agda
- src/Codata/Sized/Thunk.agda
- src/Data/AVL/IndexedMap.agda
- src/Data/Bool/Base.agda
- src/Data/Bool/Instances.agda
- + src/Data/Bool/ListAction.agda
- src/Data/Bool/Properties.agda
- src/Data/Bool/Solver.agda
- src/Data/Bytestring/Base.agda
- src/Data/Bytestring/Builder/Primitive.agda
- src/Data/Bytestring/IO.agda
- src/Data/Bytestring/IO/Primitive.agda
- src/Data/Char/Base.agda
- src/Data/Char/Instances.agda
- src/Data/Char/Properties.agda
- src/Data/Container/Combinator.agda
- src/Data/Container/Combinator/Properties.agda
- src/Data/Container/Indexed/Core.agda
- src/Data/Container/Indexed/FreeMonad.agda
- src/Data/Container/Indexed/Relation/Binary/Equality/Setoid.agda
- src/Data/Container/Indexed/Relation/Binary/Pointwise.agda
- src/Data/Container/Indexed/WithK.agda
- src/Data/Container/Membership.agda
- src/Data/Container/Morphism.agda
- src/Data/Container/Morphism/Properties.agda
- src/Data/Container/Properties.agda
- src/Data/Container/Related.agda
- src/Data/Container/Relation/Binary/Equality/Setoid.agda
- src/Data/Container/Relation/Binary/Pointwise.agda
- src/Data/Container/Relation/Unary/All.agda
- src/Data/Container/Relation/Unary/Any.agda
- src/Data/Container/Relation/Unary/Any/Properties.agda
- src/Data/DifferenceList.agda
- src/Data/DifferenceVec.agda
- src/Data/Digit.agda
- src/Data/Digit/Properties.agda
- src/Data/Empty/Polymorphic.agda
- src/Data/Fin/Base.agda
- src/Data/Fin/Induction.agda
- src/Data/Fin/Instances.agda
- src/Data/Fin/Literals.agda
- src/Data/Fin/Patterns.agda
- src/Data/Fin/Permutation.agda
- src/Data/Fin/Permutation/Components.agda
- src/Data/Fin/Properties.agda
- src/Data/Fin/Reflection.agda
- src/Data/Fin/Relation/Unary/Top.agda
- src/Data/Fin/Subset.agda
- src/Data/Fin/Subset/Induction.agda
- src/Data/Fin/Subset/Properties.agda
- src/Data/Fin/Substitution.agda
- src/Data/Fin/Substitution/Example.agda
- src/Data/Float/Base.agda
- src/Data/Float/Instances.agda
- src/Data/Float/Properties.agda
- src/Data/Graph/Acyclic.agda
- src/Data/Integer/Coprimality.agda
- src/Data/Integer/DivMod.agda
- src/Data/Integer/Divisibility.agda
- src/Data/Integer/Divisibility/Signed.agda
- src/Data/Integer/GCD.agda
- src/Data/Integer/Instances.agda
- src/Data/Integer/LCM.agda
- src/Data/Integer/Properties.agda
- src/Data/Integer/Tactic/RingSolver.agda
- src/Data/List.agda
- src/Data/List/Base.agda
- src/Data/List/Countdown.agda
- src/Data/List/Effectful.agda
- + src/Data/List/Effectful/Foldable.agda
- src/Data/List/Effectful/Transformer.agda
- src/Data/List/Extrema.agda
- src/Data/List/Extrema/Core.agda
- src/Data/List/Fresh.agda
- src/Data/List/Fresh/Membership/Setoid.agda
- src/Data/List/Fresh/Membership/Setoid/Properties.agda
- src/Data/List/Fresh/NonEmpty.agda
- src/Data/List/Fresh/Properties.agda
- src/Data/List/Fresh/Relation/Unary/All.agda
- src/Data/List/Fresh/Relation/Unary/All/Properties.agda
- src/Data/List/Fresh/Relation/Unary/Any.agda
- src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
- src/Data/List/Instances.agda
- src/Data/List/Kleene/AsList.agda
- src/Data/List/Kleene/Base.agda
- src/Data/List/Membership/DecPropositional.agda
- src/Data/List/Membership/Propositional.agda
- src/Data/List/Membership/Propositional/Properties.agda
- src/Data/List/Membership/Propositional/Properties/Core.agda
- src/Data/List/Membership/Propositional/Properties/WithK.agda
- src/Data/List/Membership/Setoid/Properties.agda
- src/Data/List/Nary/NonDependent.agda
- src/Data/List/NonEmpty/Base.agda
- src/Data/List/NonEmpty/Effectful.agda
- src/Data/List/NonEmpty/Effectful/Transformer.agda
- src/Data/List/NonEmpty/Instances.agda
- src/Data/List/NonEmpty/Properties.agda
- src/Data/List/NonEmpty/Relation/Unary/All.agda
- src/Data/List/Properties.agda
- src/Data/List/Reflection.agda
- src/Data/List/Relation/Binary/BagAndSetEquality.agda
- + src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
- src/Data/List/Relation/Binary/Disjoint/Setoid.agda
- src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
- src/Data/List/Relation/Binary/Equality/DecSetoid.agda
- src/Data/List/Relation/Binary/Equality/Propositional.agda
- src/Data/List/Relation/Binary/Equality/Setoid.agda
- src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
- src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
- src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
- src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda
- src/Data/List/Relation/Binary/Lex.agda
- src/Data/List/Relation/Binary/Lex/Core.agda
- src/Data/List/Relation/Binary/Lex/NonStrict.agda
- src/Data/List/Relation/Binary/Lex/Strict.agda
- src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
- src/Data/List/Relation/Binary/Permutation/Propositional.agda
- src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
- + src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
- src/Data/List/Relation/Binary/Permutation/Setoid.agda
- src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
- src/Data/List/Relation/Binary/Pointwise.agda
- src/Data/List/Relation/Binary/Pointwise/Properties.agda
- src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
- src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda
- + src/Data/List/Relation/Binary/Prefix/Propositional/Properties.agda
- src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
- src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
- src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
- src/Data/List/Relation/Binary/Subset/DecSetoid.agda
- src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
- src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
- + src/Data/List/Relation/Binary/Suffix/Propositional/Properties.agda
- src/Data/List/Relation/Unary/All.agda
- src/Data/List/Relation/Unary/All/Properties.agda
- + src/Data/List/Relation/Unary/All/Properties/Core.agda
- src/Data/List/Relation/Unary/AllPairs/Properties.agda
- src/Data/List/Relation/Unary/Any/Properties.agda
- src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
- src/Data/List/Relation/Unary/First.agda
- src/Data/List/Relation/Unary/First/Properties.agda
- src/Data/List/Relation/Unary/Linked.agda
- src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
- src/Data/List/Relation/Unary/Unique/Propositional.agda
- src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
- src/Data/List/Relation/Unary/Unique/Setoid.agda
- src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
- src/Data/List/Scans/Properties.agda
- src/Data/List/Solver.agda
- src/Data/List/Sort.agda
- src/Data/List/Sort/Base.agda
- + src/Data/List/Sort/InsertionSort.agda
- + src/Data/List/Sort/InsertionSort/Base.agda
- + src/Data/List/Sort/InsertionSort/Properties.agda
- src/Data/List/Sort/MergeSort.agda
- + src/Data/List/Sort/MergeSort/Base.agda
- + src/Data/List/Sort/MergeSort/Properties.agda
- src/Data/List/Zipper.agda
- src/Data/List/Zipper/Properties.agda
- src/Data/Maybe/Effectful.agda
- src/Data/Maybe/Effectful/Transformer.agda
- src/Data/Maybe/Instances.agda
- src/Data/Maybe/Properties.agda
- src/Data/Maybe/Relation/Binary/Connected.agda
- src/Data/Maybe/Relation/Binary/Pointwise.agda
- src/Data/Maybe/Relation/Unary/All.agda
- src/Data/Maybe/Relation/Unary/All/Properties.agda
- src/Data/Maybe/Relation/Unary/Any.agda
- src/Data/Nat/Base.agda
- src/Data/Nat/Binary/Base.agda
- src/Data/Nat/Binary/Properties.agda
- src/Data/Nat/Combinatorics/Specification.agda
- src/Data/Nat/Coprimality.agda
- src/Data/Nat/Divisibility/Core.agda
- src/Data/Nat/GCD.agda
- src/Data/Nat/GCD/Lemmas.agda
- src/Data/Nat/GeneralisedArithmetic.agda
- src/Data/Nat/Induction.agda
- src/Data/Nat/InfinitelyOften.agda
- src/Data/Nat/Instances.agda
- src/Data/Nat/LCM.agda
- + src/Data/Nat/ListAction.agda
- + src/Data/Nat/ListAction/Properties.agda
- src/Data/Nat/Logarithm/Core.agda
- src/Data/Nat/Primality.agda
- src/Data/Nat/Primality/Factorisation.agda
- src/Data/Nat/Properties.agda
- src/Data/Nat/Reflection.agda
- src/Data/Nat/Show.agda
- src/Data/Nat/Show/Properties.agda
- src/Data/Nat/Tactic/RingSolver.agda
- src/Data/Parity/Properties.agda
- src/Data/Product/Algebra.agda
- src/Data/Product/Effectful/Examples.agda
- src/Data/Product/Effectful/Left.agda
- src/Data/Product/Effectful/Right.agda
- src/Data/Product/Function/Dependent/Propositional.agda
- src/Data/Product/Function/Dependent/Propositional/WithK.agda
- src/Data/Product/Function/Dependent/Setoid.agda
- src/Data/Product/Instances.agda
- src/Data/Product/Nary/NonDependent.agda
- src/Data/Product/Relation/Binary/Lex/NonStrict.agda
- src/Data/Product/Relation/Binary/Lex/Strict.agda
- src/Data/Product/Relation/Binary/Pointwise/Dependent.agda
- src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
- src/Data/Rational/Base.agda
- src/Data/Rational/Instances.agda
- src/Data/Rational/Properties.agda
- src/Data/Rational/Show.agda
- src/Data/Rational/Unnormalised/Properties.agda
- src/Data/Rational/Unnormalised/Show.agda
- src/Data/Refinement.agda
- + src/Data/Refinement/Base.agda
- + src/Data/Refinement/Properties.agda
- src/Data/Refinement/Relation/Unary/All.agda
- src/Data/Sign/Properties.agda
- + src/Data/Sign/Show.agda
- src/Data/Star/BoundedVec.agda
- src/Data/Star/Decoration.agda
- src/Data/Star/Nat.agda
- src/Data/Star/Pointer.agda
- src/Data/String/Instances.agda
- src/Data/String/Properties.agda
- src/Data/String/Unsafe.agda
- src/Data/Sum/Algebra.agda
- src/Data/Sum/Effectful/Examples.agda
- src/Data/Sum/Effectful/Left.agda
- src/Data/Sum/Effectful/Left/Transformer.agda
- src/Data/Sum/Effectful/Right.agda
- src/Data/Sum/Function/Propositional.agda
- src/Data/Sum/Function/Setoid.agda
- src/Data/Sum/Instances.agda
- src/Data/Sum/Relation/Binary/LeftOrder.agda
- src/Data/Sum/Relation/Binary/Pointwise.agda
- src/Data/These/Base.agda
- src/Data/These/Effectful/Left.agda
- src/Data/These/Effectful/Left/Base.agda
- src/Data/These/Effectful/Right.agda
- src/Data/These/Effectful/Right/Base.agda
- src/Data/These/Instances.agda
- src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
- src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
- src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
- src/Data/Tree/AVL/Map/Membership/Propositional.agda
- src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
- src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
- src/Data/Tree/AVL/NonEmpty/Propositional.agda
- src/Data/Tree/Binary/Zipper.agda
- src/Data/Tree/Binary/Zipper/Properties.agda
- src/Data/Trie/NonEmpty.agda
- src/Data/Unit/Instances.agda
- src/Data/Unit/NonEta.agda
- src/Data/Unit/Polymorphic/Base.agda
- src/Data/Unit/Polymorphic/Instances.agda
- src/Data/Unit/Properties.agda
- src/Data/Universe/Indexed.agda
- src/Data/Vec/Bounded/Base.agda
- src/Data/Vec/Bounded/Show.agda
- src/Data/Vec/Effectful.agda
- + src/Data/Vec/Effectful/Foldable.agda
- src/Data/Vec/Effectful/Transformer.agda
- src/Data/Vec/Functional/Properties.agda
- src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
- src/Data/Vec/Functional/Relation/Unary/All.agda
- src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
- src/Data/Vec/Functional/Relation/Unary/Any.agda
- src/Data/Vec/Instances.agda
- src/Data/Vec/Properties.agda
- src/Data/Vec/Properties/WithK.agda
- src/Data/Vec/Recursive.agda
- src/Data/Vec/Recursive/Effectful.agda
- src/Data/Vec/Reflection.agda
- src/Data/Vec/Relation/Binary/Equality/Cast.agda
- src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda
- src/Data/Vec/Relation/Binary/Lex/Core.agda
- src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
- src/Data/Vec/Relation/Binary/Lex/Strict.agda
- src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
- src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
- src/Data/Vec/Show.agda
- src/Data/W/Indexed.agda
- src/Data/W/Sized.agda
- src/Data/W/WithK.agda
- src/Data/Word64/Instances.agda
- src/Data/Word64/Properties.agda
- src/Data/Word64/Show.agda
- src/Data/Word64/Unsafe.agda
- src/Data/Word8/Base.agda
- src/Data/Word8/Show.agda
- src/Debug/Trace.agda
- src/Effect/Applicative.agda
- src/Effect/Applicative/Indexed.agda
- src/Effect/Applicative/Predicate.agda
- src/Effect/Comonad.agda
- src/Effect/Empty.agda
- + src/Effect/Foldable.agda
- src/Effect/Functor.agda
- src/Effect/Functor/Predicate.agda
- src/Effect/Monad.agda
- src/Effect/Monad/Indexed.agda
- src/Effect/Monad/Partiality/All.agda
- src/Effect/Monad/Reader/Indexed.agda
- src/Effect/Monad/State/Indexed.agda
- src/Effect/Monad/State/Transformer/Base.agda
- src/Effect/Monad/Writer/Indexed.agda
- src/Effect/Monad/Writer/Transformer/Base.agda
- src/Foreign/Haskell.agda
- src/Foreign/Haskell/Either.agda
- src/Foreign/Haskell/List/NonEmpty.agda
- src/Foreign/Haskell/Maybe.agda
- src/Foreign/Haskell/Pair.agda
- src/Function/Base.agda
- src/Function/Bijection.agda
- src/Function/Bundles.agda
- src/Function/Consequences/Propositional.agda
- src/Function/Consequences/Setoid.agda
- src/Function/Construct/Composition.agda
- src/Function/Construct/Constant.agda
- src/Function/Construct/Identity.agda
- src/Function/Construct/Symmetry.agda
- src/Function/Endo/Propositional.agda
- src/Function/Endo/Setoid.agda
- src/Function/Endomorphism/Propositional.agda
- src/Function/Equivalence.agda
- src/Function/HalfAdjointEquivalence.agda
- src/Function/Identity/Effectful.agda
- src/Function/Injection.agda
- src/Function/Inverse.agda
- src/Function/LeftInverse.agda
- src/Function/Metric/Nat/Bundles.agda
- src/Function/Metric/Nat/Core.agda
- src/Function/Metric/Nat/Definitions.agda
- src/Function/Metric/Nat/Structures.agda
- src/Function/Nary/NonDependent.agda
- src/Function/Nary/NonDependent/Base.agda
- src/Function/Properties.agda
- src/Function/Properties/Bijection.agda
- src/Function/Properties/Equivalence.agda
- src/Function/Properties/Injection.agda
- src/Function/Properties/Inverse.agda
- src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
- src/Function/Properties/RightInverse.agda
- src/Function/Properties/Surjection.agda
- src/Function/Related.agda
- src/Function/Related/Propositional.agda
- src/Function/Related/TypeIsomorphisms.agda
- src/Function/Related/TypeIsomorphisms/Solver.agda
- src/Function/Structures/Biased.agda
- src/Function/Surjection.agda
- src/IO/Base.agda
- src/IO/Effectful.agda
- src/IO/Finite.agda
- src/IO/Infinite.agda
- src/IO/Instances.agda
- src/IO/Primitive/Finite.agda
- src/IO/Primitive/Infinite.agda
- src/Induction/InfiniteDescent.agda
- src/Induction/Lexicographic.agda
- src/Induction/WellFounded.agda
- src/Level/Literals.agda
- src/Reflection/AST/Abstraction.agda
- src/Reflection/AST/AlphaEquality.agda
- src/Reflection/AST/Argument.agda
- src/Reflection/AST/Argument/Information.agda
- src/Reflection/AST/Argument/Modality.agda
- src/Reflection/AST/Argument/Quantity.agda
- src/Reflection/AST/Argument/Relevance.agda
- src/Reflection/AST/Argument/Visibility.agda
- src/Reflection/AST/DeBruijn.agda
- src/Reflection/AST/Definition.agda
- src/Reflection/AST/Instances.agda
- src/Reflection/AST/Literal.agda
- src/Reflection/AST/Meta.agda
- src/Reflection/AST/Name.agda
- src/Reflection/AST/Show.agda
- src/Reflection/AST/Term.agda
- src/Reflection/AST/Traversal.agda
- src/Reflection/AST/Universe.agda
- src/Reflection/AnnotatedAST/Free.agda
- src/Reflection/TCM/Utilities.agda
- src/Relation/Binary/Bundles.agda
- + src/Relation/Binary/Bundles/Raw.agda
- src/Relation/Binary/Consequences.agda
- src/Relation/Binary/Construct/Add/Extrema/Equality.agda
- src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
- src/Relation/Binary/Construct/Add/Extrema/Strict.agda
- src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
- src/Relation/Binary/Construct/Add/Infimum/Strict.agda
- src/Relation/Binary/Construct/Add/Point/Equality.agda
- src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
- src/Relation/Binary/Construct/Add/Supremum/Strict.agda
- src/Relation/Binary/Construct/Closure/Equivalence/Properties.agda
- src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
- src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda
- src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
- src/Relation/Binary/Construct/Closure/Transitive.agda
- src/Relation/Binary/Construct/Composition.agda
- src/Relation/Binary/Construct/Constant.agda
- src/Relation/Binary/Construct/Constant/Core.agda
- src/Relation/Binary/Construct/Flip/EqAndOrd.agda
- src/Relation/Binary/Construct/Flip/Ord.agda
- src/Relation/Binary/Construct/Interior/Symmetric.agda
- src/Relation/Binary/Construct/Intersection.agda
- src/Relation/Binary/Construct/NaturalOrder/Left.agda
- src/Relation/Binary/Construct/NaturalOrder/Right.agda
- src/Relation/Binary/Construct/Never.agda
- src/Relation/Binary/Construct/NonStrictToStrict.agda
- src/Relation/Binary/Construct/On.agda
- src/Relation/Binary/Construct/StrictToNonStrict.agda
- src/Relation/Binary/Construct/Subst/Equality.agda
- src/Relation/Binary/Construct/Union.agda
- src/Relation/Binary/Definitions.agda
- src/Relation/Binary/HeterogeneousEquality.agda
- src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
- src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
- src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda
- src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda
- src/Relation/Binary/Indexed/Heterogeneous/Core.agda
- src/Relation/Binary/Indexed/Heterogeneous/Definitions.agda
- src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
- src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
- src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda
- src/Relation/Binary/Indexed/Homogeneous/Core.agda
- src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
- src/Relation/Binary/Indexed/Homogeneous/Structures.agda
- src/Relation/Binary/Lattice/Bundles.agda
- src/Relation/Binary/Lattice/Definitions.agda
- src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda
- src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
- src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda
- src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda
- src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda
- src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
- src/Relation/Binary/Lattice/Properties/Lattice.agda
- src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
- src/Relation/Binary/Lattice/Structures.agda
- src/Relation/Binary/Morphism/Bundles.agda
- src/Relation/Binary/Morphism/Construct/Composition.agda
- src/Relation/Binary/Morphism/Construct/Constant.agda
- src/Relation/Binary/Morphism/Construct/Identity.agda
- + src/Relation/Binary/Morphism/Construct/Product.agda
- src/Relation/Binary/Morphism/OrderMonomorphism.agda
- src/Relation/Binary/Morphism/RelMonomorphism.agda
- src/Relation/Binary/Morphism/Structures.agda
- src/Relation/Binary/OrderMorphism.agda
- src/Relation/Binary/Properties/DecTotalOrder.agda
- + src/Relation/Binary/Properties/PartialSetoid.agda
- src/Relation/Binary/Properties/Poset.agda
- src/Relation/Binary/Properties/Preorder.agda
- src/Relation/Binary/Properties/Setoid.agda
- src/Relation/Binary/Properties/StrictPartialOrder.agda
- src/Relation/Binary/Properties/StrictTotalOrder.agda
- src/Relation/Binary/Properties/TotalOrder.agda
- src/Relation/Binary/PropositionalEquality.agda
- src/Relation/Binary/PropositionalEquality/Core.agda
- src/Relation/Binary/PropositionalEquality/Properties.agda
- src/Relation/Binary/PropositionalEquality/TrustMe.agda
- src/Relation/Binary/PropositionalEquality/WithK.agda
- src/Relation/Binary/Reasoning/Base/Apartness.agda
- src/Relation/Binary/Reasoning/Base/Partial.agda
- src/Relation/Binary/Reasoning/Base/Triple.agda
- src/Relation/Binary/Reasoning/PartialSetoid.agda
- src/Relation/Binary/Reasoning/Syntax.agda
- src/Relation/Binary/Reflection.agda
- src/Relation/Binary/Rewriting.agda
- src/Relation/Binary/Structures.agda
- src/Relation/Binary/Structures/Biased.agda
- src/Relation/Nary.agda
- src/Relation/Nullary.agda
- src/Relation/Nullary/Decidable.agda
- src/Relation/Nullary/Decidable/Core.agda
- src/Relation/Nullary/Indexed/Negation.agda
- + src/Relation/Nullary/Irrelevant.agda
- src/Relation/Nullary/Negation/Core.agda
- src/Relation/Nullary/Recomputable.agda
- + src/Relation/Nullary/Recomputable/Core.agda
- src/Relation/Nullary/Reflects.agda
- src/Relation/Nullary/Universe.agda
- src/Relation/Unary.agda
- src/Relation/Unary/Algebra.agda
- src/Relation/Unary/Closure/Base.agda
- src/Relation/Unary/Closure/Preorder.agda
- src/Relation/Unary/Closure/StrictPartialOrder.agda
- src/Relation/Unary/Consequences.agda
- src/Relation/Unary/Indexed.agda
- src/Relation/Unary/Polymorphic/Properties.agda
- src/Relation/Unary/PredicateTransformer.agda
- src/Relation/Unary/Properties.agda
- src/Relation/Unary/Relation/Binary/Equality.agda
- src/Relation/Unary/Relation/Binary/Subset.agda
- src/Tactic/Cong.agda
- src/Tactic/RingSolver.agda
- src/Tactic/RingSolver/NonReflective.agda
- src/Test/Golden.agda
- src/Text/Format/Generic.agda
- standard-library.agda-lib
The diff was not included because it is too large.
View it on GitLab: https://salsa.debian.org/haskell-team/agda-stdlib/-/commit/d297d2d9ce40defd1c61113e4518b6821f70c11d
--
View it on GitLab: https://salsa.debian.org/haskell-team/agda-stdlib/-/commit/d297d2d9ce40defd1c61113e4518b6821f70c11d
You're receiving this email because of your account on salsa.debian.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://alioth-lists.debian.net/pipermail/pkg-haskell-commits/attachments/20260215/c8461b28/attachment-0001.htm>
More information about the Pkg-haskell-commits
mailing list