leanprover-community/batteries

Develop the `List.sum`, `List.prod` and related APIs

Ouverte

#1 465 ouverte le 16 oct. 2025

Voir sur GitHub
 (1 commentaire) (0 réaction) (0 personne assignée)Lean (154 forks)auto 404
enhancementhelp wanted

Métriques du dépôt

Stars
 (406 étoiles)
Métriques de merge PR
 (Merge moyen 7j 15h) (26 PRs mergées en 30 j)

Description

Mathlib's BigOperators library is well-developed, sophisticated and works extremely well. There is however a need for a less sophisticated intermediate library built directly on Std's basic classes for associativity, commutativity, identities. Just downstreaming Mathlib's API is not possible since many features don't fit in Batteries' focus on programming and formal verification.

We need a plan for this. This plan should balance low-level and high-level features, enhancing Std's basic API in a manner compatible with Mathlib's API. This plan should strengthen both Std and Mathlib, while staying within the scope of Batteries.

Guide contributeur

Direction de recherche
Explorez les implémentations existantes de List.sum et List.prod dans Std et les BigOperators de Mathlib pour concevoir une API intermédiaire qui correspond à l'accent mis par Batteries sur la programmation et la vérification formelle.
Stack technique
Aucun
Domaine
backend api design
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-2 jours
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Récente
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Investigation requise
Prérequis
LeanStdMathlib
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
20