Code

Replace signed by itv#1410

Code

Open

proux01 wants to merge 17 commits intomath-comp:mastermath-comp/analysis:masterfrom proux01:deprecate_signedproux01/analysis:deprecate_signedCopy head branch name to clipboard

+2,259-931

Commits

Commits on Jan 20, 2025

• Remove unused imports of signed.v

  proux01

  committed
  2b0a25d

  Copy full SHA for 2b0a25d

• Generalize EFin_min and EFin_max

  Show description for 9ba0c64
  proux01

  committed
  9ba0c64

  Copy full SHA for 9ba0c64

• A few lemmas to backport about min and max

  proux01

  committed
  2760837

  Copy full SHA for 2760837

• Lemma real_sqrtC to backport

  proux01

  committed
  a8e380e

  Copy full SHA for a8e380e

• Add lemmas about extended reals

  proux01

  committed
  008cb3e

  Copy full SHA for 008cb3e

• Generalize itv.v

  Show description for d5162a3
  proux01

  committed
  d5162a3

  Copy full SHA for d5162a3

• Replace notation %:inum with %:num

  proux01

  committed
  5a1cb18

  Copy full SHA for 5a1cb18

• Retrieve posnum and nonneg interfaces from signed into itv

  proux01

  committed
  0ec3b89

  Copy full SHA for 0ec3b89

• Add itv instances for min and max

  proux01

  committed
  f34513f

  Copy full SHA for f34513f

• Add instances for natmul and intmul

  proux01

  committed
  6f514db

  Copy full SHA for 6f514db

• Add instance for inv

  proux01

  committed
  a20f803

  Copy full SHA for a20f803

• Add instance for exprn

  proux01

  committed
  dc43253

  Copy full SHA for dc43253

• Add instance for norm

  proux01

  committed
  6d38582

  Copy full SHA for 6d38582

• Add instance for sqrt

  proux01

  committed
  e946e0a

  Copy full SHA for e946e0a

• Add instances on nat

  proux01

  committed
  23df0ed

  Copy full SHA for 23df0ed

• Add instances on int

  proux01

  committed
  646ed62

  Copy full SHA for 646ed62

• Port from signed to itv

  Show description for 9f4c2e5
  proux01

  committed
  9f4c2e5

  Copy full SHA for 9f4c2e5