Search results

Min and max for all total orders

Status: Open.

#1488 In UniMath/agda-unimath;

· lowasser opened on Aug 18, 2025

Uncaught ill-formed <code>concept</code> macro invocation

bugSomething isn't workingSomething isn't working

CI

Status: Open.

#1487 In UniMath/agda-unimath;

· fredrik-bakke opened on Aug 18, 2025

Interval arithmetic on the rationals

elementary-number-theory

Status: Open.

#1485 In UniMath/agda-unimath;

· lowasser opened on Aug 17, 2025

Arithmetic/geometric mean

Status: Open.

#1471 In UniMath/agda-unimath;

· lowasser opened on Aug 6, 2025

Extend arithmetic operations on a ring to Cauchy approximations on metrics on that ring

Status: Open.

#1470 In UniMath/agda-unimath;

· lowasser opened on Aug 6, 2025

Initial semiring of natural numbers

Status: Open.

#1468 In UniMath/agda-unimath;

· lowasser opened on Aug 5, 2025

Define the completion of an arbitrary metric space

metric-spaces

Status: Open.

#1458 In UniMath/agda-unimath;

· lowasser opened on Jul 25, 2025

Consider using a limit-based metric on the metric space of Cauchy approximations

metric-spaces

real-numbers

Status: Open.

#1456 In UniMath/agda-unimath;

· lowasser opened on Jul 23, 2025

Cauchy real numbers

real-numbers

Status: Open.

#1455 In UniMath/agda-unimath;

· lowasser opened on Jul 23, 2025

Consider moving sequences into <code>lists</code> package

foundation

lists

refactoring

Status: Open.

#1436 In UniMath/agda-unimath;

· lowasser opened on Jun 3, 2025

Analysis: series

elementary-number-theory

metric-spaces

real-numbers

Status: Open.

#1435 In UniMath/agda-unimath;

· lowasser opened on Jun 3, 2025

link-check accepts invalid links with unicode characters

bugSomething isn't workingSomething isn't working

CI

Status: Open.

#1434 In UniMath/agda-unimath;

· fredrik-bakke opened on May 20, 2025