Code

Refactoring positive integers#1059

Code

Merged

fredrik-bakke merged 117 commits intoUniMath:masterUniMath/agda-unimath:masterfrom malarbol:signed-integersmalarbol/agda-unimath:signed-integersCopy head branch name to clipboardMar 28, 2024

+2,900-1,035

Commits

Commits on Feb 28, 2024

• signed integers

  malarbol

  committed
  e772784

  Copy full SHA for e772784

Commits on Mar 4, 2024

• split and rename signed-integers module

  malarbol

  committed
  f68d579

  Copy full SHA for f68d579

Commits on Mar 5, 2024

• remove positivity et al. from integers module

  malarbol

  committed
  f22755b

  Copy full SHA for f22755b

• typo: put back parenthesis

  malarbol

  committed
  457dbc9

  Copy full SHA for 457dbc9

Commits on Mar 6, 2024

• redefine types

  Show description for 51bb18c
  malarbol

  committed
  51bb18c

  Copy full SHA for 51bb18c

• fix indentation

  malarbol

  committed
  afc78f3

  Copy full SHA for afc78f3

• fix indentation

  malarbol

  committed
  eb6c70d

  Copy full SHA for eb6c70d

• cleanup

  malarbol

  committed
  244c942

  Copy full SHA for 244c942

• explanation

  malarbol

  committed
  9d35ab0

  Copy full SHA for 9d35ab0

• Set properties

  malarbol

  committed
  1c7f8c3

  Copy full SHA for 1c7f8c3

• cleanup

  malarbol

  committed
  3276b51

  Copy full SHA for 3276b51

• decidability properties

  malarbol

  committed
  8dd492a

  Copy full SHA for 8dd492a

Commits on Mar 7, 2024

• rename and clean

  malarbol

  committed
  ad138be

  Copy full SHA for ad138be

• Merge branch 'UniMath:master' into signed-integers

  malarbol

  authored
  afff8f4

  Copy full SHA for afff8f4

• refactor eq-sim-unit-is-nonnegative-ℤ

  malarbol

  committed
  bb2028f

  Copy full SHA for bb2028f

• remove positivity properties from addition-integers module

  malarbol

  committed
  66e5b2c

  Copy full SHA for 66e5b2c

• Update src/elementary-number-theory/integers.lagda.md

  Show description for af888eb
  

  malarbol

  and

  fredrik-bakke

  authored
  af888eb

  Copy full SHA for af888eb

• Update src/elementary-number-theory/multiplication-integers.lagda.md

  Show description for fdb6384
  

  malarbol

  and

  fredrik-bakke

  authored
  fdb6384

  Copy full SHA for fdb6384

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for 9da8e03
  

  malarbol

  and

  fredrik-bakke

  authored
  9da8e03

  Copy full SHA for 9da8e03

• Update src/elementary-number-theory/negative-integers.lagda.md

  Show description for 509e4e5
  

  malarbol

  and

  fredrik-bakke

  authored
  509e4e5

  Copy full SHA for 509e4e5

• move single-concepts properties

  malarbol

  committed
  884f70c

  Copy full SHA for 884f70c

• cleanup

  malarbol

  committed
  bc4d715

  Copy full SHA for bc4d715

• implicit arguments and cleanup

  malarbol

  committed
  4fedaad

  Copy full SHA for 4fedaad

• addition negative integers

  malarbol

  committed
  f2b5647

  Copy full SHA for f2b5647

• shorter names

  malarbol

  committed
  5694133

  Copy full SHA for 5694133

• fix name

  malarbol

  committed
  dd7ecab

  Copy full SHA for dd7ecab

Commits on Mar 8, 2024

• remove positivity properties from multiplication-integers module

  malarbol

  committed
  a86c476

  Copy full SHA for a86c476

• fix pre-commit

  malarbol

  committed
  60d5e0d

  Copy full SHA for 60d5e0d

Commits on Mar 9, 2024

• full signed addition tables and re-organize

  malarbol

  committed
  6bbd474

  Copy full SHA for 6bbd474

• fix typo

  malarbol

  committed
  2a40405

  Copy full SHA for 2a40405

• full signed multiplication table and rules

  malarbol

  committed
  ef992b7

  Copy full SHA for ef992b7

• refactor for illustration

  malarbol

  committed
  2aaceba

  Copy full SHA for 2aaceba

• descriptive headers

  malarbol

  committed
  862aded

  Copy full SHA for 862aded

• fix typo

  malarbol

  committed
  cbc83f2

  Copy full SHA for cbc83f2

• strict inequality implies inequality

  malarbol

  committed
  eb3e0bf

  Copy full SHA for eb3e0bf

• re-organize inequality integers

  malarbol

  committed
  2ddec64

  Copy full SHA for 2ddec64

• move is-nonzero-is-positive-ℤ

  malarbol

  committed
  65b1d01

  Copy full SHA for 65b1d01

• signed neg-ℤ

  malarbol

  committed
  ce731bf

  Copy full SHA for ce731bf

Commits on Mar 10, 2024

• fix names, headers and re-organize

  malarbol

  committed
  5251cf4

  Copy full SHA for 5251cf4

• remove negatives-add-ℤ

  malarbol

  committed
  0e612c4

  Copy full SHA for 0e612c4

• fix names and types

  malarbol

  committed
  8104bba

  Copy full SHA for 8104bba

• fix indentation

  malarbol

  committed
  40ba992

  Copy full SHA for 40ba992

• canonical equivalences between natural numbers and signed integers

  malarbol

  committed
  bc1474b

  Copy full SHA for bc1474b

• remove unused imports

  malarbol

  committed
  2b4b03e

  Copy full SHA for 2b4b03e

• cleanup

  malarbol

  committed
  37ff62f

  Copy full SHA for 37ff62f

• strict inequality implies inequality

  malarbol

  committed
  7b917db

  Copy full SHA for 7b917db

Commits on Mar 11, 2024

• fix indentation

  malarbol

  committed
  f222c99

  Copy full SHA for f222c99

• decidability of orderings

  malarbol

  committed
  7a13a34

  Copy full SHA for 7a13a34

Commits on Mar 16, 2024

• fix names and type signatures

  malarbol

  committed
  e4b4713

  Copy full SHA for e4b4713

Commits on Mar 19, 2024

• Update src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md

  Show description for 70d87ba
  

  malarbol

  and

  fredrik-bakke

  authored
  70d87ba

  Copy full SHA for 70d87ba

• Update src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md

  Show description for cb34096
  

  malarbol

  and

  fredrik-bakke

  authored
  cb34096

  Copy full SHA for cb34096

• Update src/elementary-number-theory/reduced-integer-fractions.lagda.md

  Show description for a6290a8
  

  malarbol

  and

  fredrik-bakke

  authored
  a6290a8

  Copy full SHA for a6290a8

• Update src/elementary-number-theory/nonzero-integers.lagda.md

  Show description for 84d51f6
  

  malarbol

  and

  fredrik-bakke

  authored
  84d51f6

  Copy full SHA for 84d51f6

• Update src/elementary-number-theory/positive-integers.lagda.md

  Show description for 04da8db
  

  malarbol

  and

  fredrik-bakke

  authored
  04da8db

  Copy full SHA for 04da8db

• Update src/elementary-number-theory/positive-integers.lagda.md

  Show description for 3854c4e
  

  malarbol

  and

  fredrik-bakke

  authored
  3854c4e

  Copy full SHA for 3854c4e

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for dc0f5cf
  

  malarbol

  and

  fredrik-bakke

  authored
  dc0f5cf

  Copy full SHA for dc0f5cf

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for 47bea08
  

  malarbol

  and

  fredrik-bakke

  authored
  47bea08

  Copy full SHA for 47bea08

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for 2179a9d
  

  malarbol

  and

  fredrik-bakke

  authored
  2179a9d

  Copy full SHA for 2179a9d

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for 09c7c3e
  

  malarbol

  and

  fredrik-bakke

  authored
  09c7c3e

  Copy full SHA for 09c7c3e

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for a1020b4
  

  malarbol

  and

  fredrik-bakke

  authored
  a1020b4

  Copy full SHA for a1020b4

• Update src/elementary-number-theory/inequality-integers.lagda.md

  Show description for 772f45a
  

  malarbol

  and

  fredrik-bakke

  authored
  772f45a

  Copy full SHA for 772f45a

• Update src/elementary-number-theory/mediant-integer-fractions.lagda.md

  Show description for 0709cf1
  

  malarbol

  and

  fredrik-bakke

  authored
  0709cf1

  Copy full SHA for 0709cf1

• Apply suggestions from code review

  Show description for 403ffb7
  

  malarbol

  and

  fredrik-bakke

  authored
  403ffb7

  Copy full SHA for 403ffb7

• Update src/elementary-number-theory/positive-integers.lagda.md

  Show description for 13b2859
  

  malarbol

  and

  fredrik-bakke

  authored
  13b2859

  Copy full SHA for 13b2859

• fix name

  malarbol

  committed
  cabd20a

  Copy full SHA for cabd20a

Commits on Mar 23, 2024

• WIP review

  malarbol

  committed
  6a9924a

  Copy full SHA for 6a9924a

• strict-inequality-integers module

  malarbol

  committed
  8fc4f59

  Copy full SHA for 8fc4f59

• decidable total order integers

  malarbol

  committed
  184a3fd

  Copy full SHA for 184a3fd

• fix headers

  malarbol

  committed
  ec06c68

  Copy full SHA for ec06c68

• lint

  malarbol

  committed
  593311e

  Copy full SHA for 593311e

• decidable total order rational numbers

  malarbol

  committed
  7b4eadb

  Copy full SHA for 7b4eadb

• reorganize

  malarbol

  committed
  7d930ad

  Copy full SHA for 7d930ad

• see also

  malarbol

  committed
  d80f95d

  Copy full SHA for d80f95d

• headers

  malarbol

  committed
  f06dd2e

  Copy full SHA for f06dd2e

• fix headers (concepts)

  malarbol

  committed
  af2318b

  Copy full SHA for af2318b

• strict-inequality-rational-numbers

  malarbol

  committed
  fdf34ac

  Copy full SHA for fdf34ac

• Merge branch 'master' into signed-integers

  malarbol

  authored
  7bd0623

  Copy full SHA for 7bd0623

• fix name

  malarbol

  committed
  7de3d93

  Copy full SHA for 7de3d93

• cleanup ideas

  malarbol

  committed
  ee1cc1b

  Copy full SHA for ee1cc1b

Commits on Mar 25, 2024

• strict inequality on integer fractions

  malarbol

  committed
  4e1f7bf

  Copy full SHA for 4e1f7bf

• fix typo fractions-Z / fraction-Z

  malarbol

  committed
  1fcd3a2

  Copy full SHA for 1fcd3a2

• fix typo fractions-Z / fraction-Z

  malarbol

  committed
  068bf80

  Copy full SHA for 068bf80

• fix broken link

  malarbol

  committed
  a6278be

  Copy full SHA for a6278be

• fix broken link

  malarbol

  committed
  8b4c716

  Copy full SHA for 8b4c716

• Merge branch 'master' into signed-integers

  malarbol

  authored
  4b8e6f1

  Copy full SHA for 4b8e6f1

Commits on Mar 26, 2024

• Merge branch 'master' into signed-integers

  malarbol

  authored
  4d17292

  Copy full SHA for 4d17292

Commits on Mar 27, 2024

• Update src/elementary-number-theory/inequality-integers.lagda.md

  Show description for 764c324
  

  malarbol

  and

  fredrik-bakke

  authored
  764c324

  Copy full SHA for 764c324

• Update src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md

  Show description for 2c6f06f
  

  malarbol

  and

  fredrik-bakke

  authored
  2c6f06f

  Copy full SHA for 2c6f06f

• Update src/elementary-number-theory/strict-inequality-integers.lagda.md

  Show description for a7ce8fe
  

  malarbol

  and

  fredrik-bakke

  authored
  a7ce8fe

  Copy full SHA for a7ce8fe

• Update src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md

  Show description for 0c84e91
  

  malarbol

  and

  fredrik-bakke

  authored
  0c84e91

  Copy full SHA for 0c84e91

• Update src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md

  Show description for 930dcc8
  

  malarbol

  and

  fredrik-bakke

  authored
  930dcc8

  Copy full SHA for 930dcc8

• Update src/elementary-number-theory/positive-integers.lagda.md

  Show description for 2570928
  

  malarbol

  and

  fredrik-bakke

  authored
  2570928

  Copy full SHA for 2570928

• Update src/elementary-number-theory/positive-and-negative-integers.lagda.md

  Show description for dab2c55
  

  malarbol

  and

  fredrik-bakke

  authored
  dab2c55

  Copy full SHA for dab2c55

• Update src/elementary-number-theory/nonnegative-integers.lagda.md

  Show description for 3070b77
  

  malarbol

  and

  fredrik-bakke

  authored
  3070b77

  Copy full SHA for 3070b77

• Apply suggestions from code review

  Show description for 3f8bd30
  

  malarbol

  and

  fredrik-bakke

  authored
  3f8bd30

  Copy full SHA for 3f8bd30

• Update src/elementary-number-theory/addition-integers.lagda.md

  Show description for 2d04be0
  

  malarbol

  and

  fredrik-bakke

  authored
  2d04be0

  Copy full SHA for 2d04be0

• Update src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md

  Show description for 4424681
  

  malarbol

  and

  fredrik-bakke

  authored
  4424681

  Copy full SHA for 4424681

• Update src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md

  Show description for 588c9b5
  

  malarbol

  and

  fredrik-bakke

  authored
  588c9b5

  Copy full SHA for 588c9b5

• Update src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md

  Show description for dd96315
  

  malarbol

  and

  fredrik-bakke

  authored
  dd96315

  Copy full SHA for dd96315

• Update src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md

  Show description for 3729baa
  

  malarbol

  and

  fredrik-bakke

  authored
  3729baa

  Copy full SHA for 3729baa

• fix parentheses

  Show description for 2c40345
  

  malarbol

  and

  fredrik-bakke

  authored
  2c40345

  Copy full SHA for 2c40345

• Update src/elementary-number-theory/inequality-integers.lagda.md

  Show description for 9b4ff03
  

  malarbol

  and

  fredrik-bakke

  authored
  9b4ff03

  Copy full SHA for 9b4ff03

• Update src/elementary-number-theory/integers.lagda.md

  Show description for 8b16ac2
  

  malarbol

  and

  fredrik-bakke

  authored
  8b16ac2

  Copy full SHA for 8b16ac2

• fix headers

  Show description for f4a477f
  

  malarbol

  and

  fredrik-bakke

  authored
  f4a477f

  Copy full SHA for f4a477f

• fix headers

  Show description for 27ed6d3
  

  malarbol

  and

  fredrik-bakke

  authored
  27ed6d3

  Copy full SHA for 27ed6d3

• Update src/elementary-number-theory/inequality-natural-numbers.lagda.md

  Show description for edab26f
  

  malarbol

  and

  fredrik-bakke

  authored
  edab26f

  Copy full SHA for edab26f

• lint

  malarbol

  committed
  309aa1a

  Copy full SHA for 309aa1a

• fix see also

  malarbol

  committed
  05421f4

  Copy full SHA for 05421f4

• strict inequality on integer fractions is dense and located

  malarbol

  committed
  e89a650

  Copy full SHA for e89a650

Commits on Mar 28, 2024

• fix parentheses

  malarbol

  committed
  f4d365e

  Copy full SHA for f4d365e

• better header

  malarbol

  committed
  cd2de6b

  Copy full SHA for cd2de6b

• fix inequality headers

  malarbol

  committed
  5bc5f96

  Copy full SHA for 5bc5f96

• Update src/elementary-number-theory/inequality-integer-fractions.lagda.md

  Show description for 5823072
  

  malarbol

  and

  fredrik-bakke

  authored
  5823072

  Copy full SHA for 5823072

• Update src/elementary-number-theory/inequality-integer-fractions.lagda.md

  Show description for ee50426
  

  malarbol

  and

  fredrik-bakke

  authored
  ee50426

  Copy full SHA for ee50426

• fix headers

  malarbol

  committed
  dc16837

  Copy full SHA for dc16837

• fix headers -- remove standard

  malarbol

  committed
  cce4d39

  Copy full SHA for cce4d39

• Apply suggestions from code review

  Show description for 794197c
  

  malarbol

  and

  fredrik-bakke

  authored
  794197c

  Copy full SHA for 794197c