Search results

Remove <code>bigmaxr</code> from <code>Rstruct.v</code>?

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1739 In math-comp/analysis;

· affeldt-aist opened on Oct 24, 2025

· 

1.14.0

rename <code>adjacent</code> into <code>adjacent_seq</code>

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1735 In math-comp/analysis;

· affeldt-aist opened on Oct 20, 2025

· 

1.14.0

proposal renaming for <code>derivable_oo_continuous_bnd</code>

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1734 In math-comp/analysis;

· affeldt-aist opened on Oct 9, 2025

· 

1.14.0

<code>ln_eq0</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1733 In math-comp/analysis;

· affeldt-aist opened on Oct 8, 2025

· 

1.14.0

Please pick the version you prefer for Rocq 9.0 in Rocq Platform 2025.09

Status: Open.

#1711 In math-comp/analysis;

· Justme0606 opened on Aug 29, 2025

'exprn' and 'expr' naming inconsistency in derive.v

Status: Open.

#1677 In math-comp/analysis;

· yosakaon opened on Jul 7, 2025

use <code>addrK</code>, ..., <code>divKf</code>, ... to shorten scripts

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1667 In math-comp/analysis;

· affeldt-aist opened on Jul 2, 2025

· 

1.14.0

improve the interface for the product measure

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1665 In math-comp/analysis;

· affeldt-aist opened on Jul 1, 2025

· 

1.14.0

Double-check local notations in <code>hoelder.v</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Open.

#1644 In math-comp/analysis;

· affeldt-aist opened on Jun 19, 2025

· 

1.14.0

<code>Lnorm0</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Open.

#1643 In math-comp/analysis;

· affeldt-aist opened on Jun 19, 2025

· 

1.14.0

Rewriting under <code>cvg_to</code> Fails

Status: Open.

#1634 In math-comp/analysis;

· Yosuke-Ito-345 opened on May 26, 2025

Updating instances of <code>ae</code> and <code>near</code> notations

Status: Open.

#1617 In math-comp/analysis;

· hoheinzollern opened on May 12, 2025