All pull requests

Pull requests

• Fill in some implicit arguments in Data.Nat.DivMod

  #3122·shhyou opened Sep 24, 2026Contributor·

  ·
  3

• Vec recusive

  #3120·jkopanski opened Sep 17, 2026Contributor·

  ·

• [ add ] More Data.Product.Nary.NonDependent operation and properties

  #3119·jkopanski opened Sep 17, 2026Contributor·

  ·

• Add antisym-≡ to Data.Vec.Relation.Binary.Pointwise.Inductive

  #3117·Taneb opened Sep 10, 2026Member·

  ·
  4

• [ add ] Data.Vec.Recursive.Relation.Binary.Pointwise

  additionlibrary-design
  #3110·jkopanski opened Aug 27, 2026Contributor·

  ·
  5

• Another Prop experiment

  #3108·Taneb opened Aug 11, 2026Member·

  ·
  1

• Add negatives for commutative monoids and semirings (Abelian group and ring completions)

  #3106·LionOfJewdah opened Aug 5, 2026·

  ·
  16

• Add Show class

  #3098·silas-hw opened Jul 30, 2026Contributor·

  ·
  1

  27

• [ refactor ] make Data.List.Base.[_] a pattern synonym

  breakingdiscussionlibrary-designnamingrefactoring
  #3095·jamesmckinna opened Jul 30, 2026Collaborator·

  ·
  7

• [ refactor ] rename constructors of Data.List.Base.InitLast and friends

  breakingcosmeticdeprecationrefactoringstatus: blocked-by-issuestyle-guide
  #3090·jamesmckinna opened Jul 26, 2026Collaborator·

  ·

  · v3.0
  1

• strengthen the AVL tree's insertWith-just

  breakingrefactoring
  #3087·mikedelorimier opened Jul 23, 2026Contributor·

  ·
  9

• Add colour to defunct-readme.sh and ignore .git

  #3086·silas-hw opened Jul 23, 2026Contributor·

  ·
  2

• [ refactor ] generalise Data.Sum.Relation.Binary.Pointwise.elim #3079

  additionrefactoring
  #3085·jamesmckinna opened Jul 23, 2026Collaborator·

  ·

  · v3.0
  8

• Add Queue datatype

  #3084·silas-hw opened Jul 20, 2026Contributor·

  ·
  1

  128

• Add defunct-readme check to CI

  #3080·silas-hw opened Jul 16, 2026Contributor·

  ·
  1

  1

• [ add ] Pointwise lifting of algebra to Data.Vec.Functional

  addition
  #3077·JacquesCarette opened Jul 16, 2026Collaborator·

  ·
  6

• [ draft ] Refactor Dec to use constructive negation

  refactoring
  #3065·gallais opened Jul 9, 2026Member·

  ·

  · v3.0
  12

• [ add ] syntax for antisym equality reasoning in Relation.Binary.Reasoning.PartialOrder #3047

  additionlow-hanging-fruitpriority:lo
  #3057·jamesmckinna opened Jul 8, 2026Collaborator·

  ·
  1

  6

• [ add ] Data.List.Base.foldMap and refactor

  additionrefactoring
  #3026·jamesmckinna opened Jun 20, 2026Collaborator·

  ·

  · v3.0
  1

  12

• [ add ] Natural number square root

  addition
  #3023·jamesmckinna opened Jun 18, 2026Collaborator·

  ·
  1

  14

• Make final parameter of Acc an index

  discussionmikan
  #3020·Taneb opened Jun 18, 2026Member·

  ·
  8

• Make irrelevant-recompute unsafe

  #3012·jespercockx opened Jun 10, 2026Member·

  ·
  10

• Add definitions for function-like relations

  addition
  #3001·Taneb opened Jun 5, 2026Member·

  ·
  2

• Replace irrelevance with Prop

  #2998·jespercockx opened May 27, 2026Member·

  ·
  17

• [ fix ] #2865 for the remaining Data.*.Relation.Unary.Any

  deprecationnaming
  #2972·jamesmckinna opened Apr 1, 2026Collaborator·

  ·
  4