leanprover-community/batteries

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

Aperta

#1465 aperta il 16 ott 2025

Vedi su GitHub
 (1 commento) (0 reazioni) (0 assegnatari)Lean (154 fork)auto 404
enhancementhelp wanted

Metriche repository

Star
 (406 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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.

Guida contributor

Direzione di ricerca
Esplora le implementazioni esistenti di List.sum e List.prod in Std e i BigOperators di Mathlib per progettare un'API intermedia che si adatti al focus di Batteries sulla programmazione e la verifica formale.
Tech stack
Nessuno
Dominio
backend api design
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Nuova
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Richiede indagine
Prerequisiti
LeanStdMathlib
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
20