GitHub · Where software is built

Labels Milestones New issue

[ design ] use higher-level programming abstractions

#2834

· jamesmckinna opened

on Sep 29, 2025

[ design ] Re-exports from <code>Algebra.Properties.X</code>

#2804

· jamesmckinna opened

on Aug 4, 2025

[ refactor ] make <code>contradiction</code> and friends entirely definitionally proof-irrelevant

status: blocked-by-issue

agda/agda-stdlib

#2802

· jamesmckinna opened

on Aug 4, 2025

·

[ discussion ] alternative design for <code>Algebra.Structures.IsX</code> and <code>Algebra.Properties.X</code>

agda/agda-stdlib

#2762

· jamesmckinna opened

on Jul 9, 2025

·

hypothetical-rewrite

[ definition ] characteristic of a <code>Ring</code> (etc.)

#2760

· jamesmckinna opened

on Jul 7, 2025

Implementation of consequences and lemmas for Groups

#2695

· jmougeot opened

on Apr 11, 2025

Document use of Unicode symbols on a per-module basis

#2690

· jamesmckinna opened

on Apr 8, 2025

[ refactor ] rationalise the common APIs for <code>List</code> and <code>Vec</code> versions of <code>Data..Relation.Binary.Lex.</code>

#2687

· jamesmckinna opened

on Mar 28, 2025

·

Snoclists?

#2684

· gallais opened

on Mar 21, 2025

Left/Right inconsistency

#2654

· JacquesCarette opened

on Mar 12, 2025

[ refactor ] Reconcile <code>Relation.Binary.Definitions.Adjoint</code> and <code>Function.Definitions.Inverse*</code>

#2581

· jamesmckinna opened

on Feb 10, 2025

[ refactor ] Revise definitions, consequences, and use, of <code>Algebra.Definitions.(Almost)*Cancellative</code>

agda/agda-stdlib

#2573

· jamesmckinna opened

on Feb 6, 2025

·