Code

Rational order#1071

Code

Merged

mortberg merged 10 commits intoagda:masteragda/cubical:masterfrom LuuBluum:RationalOrderLuuBluum/cubical:RationalOrderCopy head branch name to clipboardNov 2, 2023

+2,397-167

Commits

Commits on Sep 18, 2023

• Adjust Rationals to use Int instead of QuoInt

  LuuBluum

  committed
  02c912f

  Copy full SHA for 02c912f

Commits on Oct 18, 2023

• Define ordering over rationals and basic properties

  LuuBluum

  committed
  7a92756

  Copy full SHA for 7a92756

Commits on Oct 26, 2023

• More properties of rational order

  LuuBluum

  committed
  db32f58

  Copy full SHA for db32f58

• Clean up definition of order; define trichotomy

  LuuBluum

  committed
  ca40e3e

  Copy full SHA for ca40e3e

Commits on Oct 27, 2023

• Add multiplication cancelling to rationals

  LuuBluum

  committed
  b10112f

  Copy full SHA for b10112f

Commits on Oct 28, 2023

• Merge branch 'agda:master' into RationalOrder

  LuuBluum

  authored
  4d84779

  Copy full SHA for 4d84779

• Fix whitespace

  LuuBluum

  committed
  0a523ac

  Copy full SHA for 0a523ac

Commits on Oct 30, 2023

• Merge branch 'agda:master' into RationalOrder

  LuuBluum

  authored
  d9494fa

  Copy full SHA for d9494fa

• Remove unnecessary 0<1 proof

  LuuBluum

  committed
  9165d32

  Copy full SHA for 9165d32

• Redefine rec2 with pattern matching

  LuuBluum

  committed
  1bc03c7

  Copy full SHA for 1bc03c7