Search results

Reify the style-guide as a 'linter'?

admin

continuous-integration

library-design

Status: Open.

#2923 In agda/agda-stdlib;

· jamesmckinna opened on Jan 26, 2026

4 proofs suggested for Rational.Properties

Status: Open.

#2921 In agda/agda-stdlib;

· mechvel opened on Jan 24, 2026

[ deprecate ] one of <code>Function.Core</code> *or* <code>Algebra.Core</code>

bikeshedding

deprecation

Status: Open.

#2917 In agda/agda-stdlib;

· jamesmckinna opened on Jan 23, 2026

[ add ] <code>Algebra.Module.Construct.Pointwise</code>, following <code>Algebra.Construct.Pointwise</code>

addition

Status: Open.

#2915 In agda/agda-stdlib;

· jamesmckinna opened on Jan 23, 2026

[ add ] functorial change-of-base from <code>S-YModule</code> to <code>R-YModule</code> induced by an <code>XRing</code> homomorphism from <code>R</code> to <code>S</code>

addition

Status: Open.

#2913 In agda/agda-stdlib;

· jamesmckinna opened on Jan 23, 2026

Suggestion with <code>Preserves</code> for two predicates

addition

discoverabilityHow easy/hard will it be for users to find, within the context of their application?How easy/hard will it be for users to find, within the context of their application?

Fairbairn thresholdThe contribution is 'too small' to merit the overheadThe contribution is 'too small' to merit the overhead

library-design

Status: Open.

#2909 In agda/agda-stdlib;

· mechvel opened on Jan 17, 2026

Inline <code>Data.Vec.Functional.map</code> for Better Termination Checking

Status: Open.

#2905 In agda/agda-stdlib;

· david-davies opened on Jan 4, 2026

where are relations between <code>⊎, ×, ¬</code>

Status: Open.

#2898 In agda/agda-stdlib;

· mechvel opened on Dec 7, 2025

Remove needless dependencies using the new Agda option

dependencies

task

Status: Open.

#2897 In agda/agda-stdlib;

· gallais opened on Dec 1, 2025

Generated websites

continuous-integration

discoverabilityHow easy/hard will it be for users to find, within the context of their application?How easy/hard will it be for users to find, within the context of their application?

documentation

Status: Open.

#2893 In agda/agda-stdlib;

· pdmosses opened on Nov 24, 2025

[ refactor/design ] left- and right- actions of normal subgroups on their ambient group

Status: Open.

#2892 In agda/agda-stdlib;

· jamesmckinna opened on Nov 24, 2025

[ add ] <code>INT</code> view of <code>Data.Integer.Base.ℤ</code>

addition

library-design

refactoring

views

Status: Open.

#2890 In agda/agda-stdlib;

· jamesmckinna opened on Nov 21, 2025