List view

Migrate <code>_↔̇_</code> to the new Function hierarchy + more arrows for indexed sets

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1982

#1982 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 19, 2023

Get rid of redundant deps in <code>System.Console.ANSI</code>

bug

dependencies

Status: Merged (completed).

agda/agda-stdlibnumber 1994

#1994 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 19, 2023

Refactoring (inversion) properties of <code>_&lt;_</code> on <code>Nat</code>, plus consequences

addition

refactoring

regression

Status: Merged (completed).

agda/agda-stdlibnumber 2000

#2000 In agda/agda-stdlib;

· by jamesmckinna was closed on Oct 12, 2023

Simplify <code>Data.Product</code> imports

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2003

#2003 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 30, 2023

Eliminate many propositional equality imports

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2002

#2002 In agda/agda-stdlib;

· by Taneb was closed on Jul 6, 2023

Cut down <code>Function</code> imports

dependencies

Status: Merged (completed).

agda/agda-stdlibnumber 2006

#2006 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 28, 2023

Simplify <code>Data.List</code> imports

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2007

#2007 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 30, 2023

Fixities for <code>Function</code>, <code>Data</code>, and <code>Reflection</code>

bug

Status: Merged (completed).

agda/agda-stdlibnumber 1987

#1987 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 19, 2023

[ re #1993 ] Simplifying the dependency graph

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 1995

#1995 In agda/agda-stdlib;

· by gallais was closed on Jun 27, 2023

Fractional (1.5) fixity for <code>Relation.Nullary.¬_</code>

breaking

library-design

status: won't-mergeDecided against merging the PR in.Decided against merging the PR in.

Status: Closed (abandoned).

agda/agda-stdlibnumber 1999

#1999 In agda/agda-stdlib;

· by Saransh-cpp was closed on Aug 11, 2023

More fixities

bug

Status: Merged (completed).

agda/agda-stdlibnumber 2008

#2008 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 30, 2023

gitignore <code>_build</code> correctly

admin

Status: Merged (completed).

agda/agda-stdlibnumber 2010

#2010 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 30, 2023

Reconciling <code>Data.Nat.Divisibility.Core._∣_</code> and <code>Algebra.Definitions.RawMagma._∣_</code>

cosmetic

discussion

library-design

low-hanging-fruit

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2013

#2013 In agda/agda-stdlib;

· by jamesmckinna was closed on Jul 29, 2023

Fixities for <code>Data</code> and <code>Codata</code>

bug

Status: Merged (completed).

agda/agda-stdlibnumber 1989

#1989 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 20, 2023

Update CHANGELOG.md move 2 functions to section Data.List.Properties

documentation

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 1991

#1991 In agda/agda-stdlib;

· by Sofia-Insa was closed on Jun 19, 2023

Fixities for <code>Relation</code> and <code>Algebra</code>

bug

Status: Merged (completed).

agda/agda-stdlibnumber 1992

#1992 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 27, 2023

Fixities for <code>Data</code> and <code>Codata</code>

bug

Status: Merged (completed).

agda/agda-stdlibnumber 1985

#1985 In agda/agda-stdlib;

· by Saransh-cpp was closed on Jun 19, 2023

functions <code>take/drop/head -map-commute</code> added to stdl Data.List.Properties

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1986

#1986 In agda/agda-stdlib;

· by Sofia-Insa was closed on Jul 31, 2023

added new function <code>take-all</code> to stdl

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1983

#1983 In agda/agda-stdlib;

· by Sofia-Insa was closed on Jun 27, 2023

New functions <code>take-drop-1</code> and <code>take-one-more</code> added to Data.List.Properties

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1984

#1984 In agda/agda-stdlib;

· by Sofia-Insa was closed on Jun 28, 2023

Wrapping Comments &amp; Fixing Code Delimiters

documentation

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2015

#2015 In agda/agda-stdlib;

· by mglst was closed on Jul 29, 2023

Move <code>≡-setoid</code> to <code>Function.Indexed.Relation.Binary.Equality</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2047

#2047 In agda/agda-stdlib;

· by Saransh-cpp was closed on Sep 13, 2023

Sync <code>iterate</code> and <code>replicate</code> for <code>List</code> and <code>Vec</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2051

#2051 In agda/agda-stdlib;

· by Saransh-cpp was closed on Oct 4, 2023

Final <code>Data.Product</code> import simplifications

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2052

#2052 In agda/agda-stdlib;

· by Saransh-cpp was closed on Aug 11, 2023

Add more properties for <code>xor</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2035

#2035 In agda/agda-stdlib;

· by Saransh-cpp was closed on Aug 11, 2023