Code

Similarity of real numbers#1301

Code

Merged

fredrik-bakke merged 10 commits intoUniMath:masterUniMath/agda-unimath:masterfrom lowasser:similar-realslowasser/agda-unimath:similar-realsCopy head branch name to clipboardFeb 9, 2025

+105

Commits

Commits on Feb 8, 2025

• Start defining similarity

  lowasser

  committed
  e4c94be

  Copy full SHA for e4c94be

• Merge branch 'master' into similar-reals

  lowasser

  committed
  0d3d908

  Copy full SHA for 0d3d908

• make pre-commit

  lowasser

  committed
  e31f172

  Copy full SHA for e31f172

• Remove unused import

  lowasser

  committed
  53fa7f3

  Copy full SHA for 53fa7f3

• Apply suggestions from code review

  Show description for c991bbb
  

  lowasser

  and

  fredrik-bakke

  authored
  c991bbb

  Copy full SHA for c991bbb

• make pre-commit

  lowasser

  committed
  40677d3

  Copy full SHA for 40677d3

• Merge branch 'master' into similar-reals

  lowasser

  committed
  df0c51a

  Copy full SHA for df0c51a

• Fix import

  lowasser

  committed
  afc2884

  Copy full SHA for afc2884

Commits on Feb 9, 2025

• Apply suggestions from code review

  Show description for ec9ed6f
  

  lowasser

  and

  fredrik-bakke

  authored
  ec9ed6f

  Copy full SHA for ec9ed6f

• Merge branch 'master' into similar-reals

  lowasser

  authored
  4e3513c

  Copy full SHA for 4e3513c