Code

Redefines Data.Nat.Base._≤″_#1948

Code

Merged

MatthewDaggitt merged 20 commits intoagda:masteragda/agda-stdlib:masterfrom jamesmckinna:issue1919jamesmckinna/agda-stdlib:issue1919Copy head branch name to clipboardOct 4, 2023

Commits

Commits on Apr 22, 2023

• introduced alternative definitions; revised one usage of previous one

  jamesmckinna

  committed
  0adbbe8

  Copy full SHA for 0adbbe8

• deprecated field name (NB tricky)

  jamesmckinna

  committed
  b62ef81

  Copy full SHA for b62ef81

• installed new definition

  jamesmckinna

  committed
  8993f59

  Copy full SHA for 8993f59

• removed old definition; tidied up

  jamesmckinna

  committed
  7f09808

  Copy full SHA for 7f09808

• CHANGELOG plus portable definition of the proof projection

  jamesmckinna

  committed
  221ac92

  Copy full SHA for 221ac92

• CHANGELOG

  jamesmckinna

  committed
  5935db4

  Copy full SHA for 5935db4

• more explicit deprecation warning

  jamesmckinna

  committed
  829ddd5

  Copy full SHA for 829ddd5

Commits on Apr 23, 2023

• typo in CHANGELOG

  jamesmckinna

  committed
  e9c7170

  Copy full SHA for e9c7170

• exchnaged repeated recursive for a nested irrefutbale with pattern

  jamesmckinna

  committed
  824dce6

  Copy full SHA for 824dce6

• Merge branch 'issue1919' of https://github.com/jamesmckinna/agda-stdlib into issue1919

  jamesmckinna

  committed
  dbfb5a7

  Copy full SHA for dbfb5a7

• Revert "Merge branch 'issue1919' of https://github.com/jamesmckinna/agda-stdlib into issue1919"

  Show description for 61ef3f0
  jamesmckinna

  committed
  61ef3f0

  Copy full SHA for 61ef3f0

• Revert "exchnaged repeated recursive for a nested irrefutbale with pattern"

  Show description for 693270e
  jamesmckinna

  committed
  693270e

  Copy full SHA for 693270e

Commits on Apr 25, 2023

• tweaks

  jamesmckinna

  committed
  f120c1e

  Copy full SHA for f120c1e

Commits on May 12, 2023

• Update CHANGELOG.md

  Show description for c1edba4
  

  jamesmckinna

  and

  gallais

  authored
  c1edba4

  Copy full SHA for c1edba4

Commits on Aug 4, 2023

• removed deprecation wart in favour of new definition in Data.Nat.Properties

  jamesmckinna

  committed
  519dde4

  Copy full SHA for 519dde4

• resolved merge conflict

  jamesmckinna

  committed
  9d451b9

  Copy full SHA for 9d451b9

• removed now-spurious hiding directive

  jamesmckinna

  committed
  1c94a46

  Copy full SHA for 1c94a46

• corrected CHANGELOG

  jamesmckinna

  committed
  b44100f

  Copy full SHA for b44100f

• Merge branch 'master' into issue1919

  jamesmckinna

  authored
  fd163b5

  Copy full SHA for fd163b5

Commits on Aug 8, 2023

• make equivalence proof ≤″⇒≤‴ more lazy

  jamesmckinna

  committed
  056fec1

  Copy full SHA for 056fec1