Code

Vec.Properties: introduce ≈-cong′#2424

Code

Merged

MatthewDaggitt merged 8 commits intoagda:masteragda/agda-stdlib:masterfrom mildsunrise:vec-congmildsunrise/agda-stdlib:vec-congCopy head branch name to clipboardJan 3, 2025

Commits

Commits on Jan 2, 2025

• Vec.Properties: introduce ≈-cong′

  mildsunrise

  committed
  7f9cb1f

  Copy full SHA for 7f9cb1f

• derive cast-* lemmas from it

  mildsunrise

  committed
  c6101ed

  Copy full SHA for c6101ed

• use it in proofs

  mildsunrise

  committed
  888a8c9

  Copy full SHA for 888a8c9

• match m and n before the Vecs

  mildsunrise

  committed
  f6cffb3

  Copy full SHA for f6cffb3

• convert Cast's implicit module param to variable

  Show description for 67b1a49
  mildsunrise

  committed
  67b1a49

  Copy full SHA for 67b1a49

• move ≈-cong′ to Cast

  mildsunrise

  committed
  387a130

  Copy full SHA for 387a130

• add changelog entry

  mildsunrise

  committed
  09530bd

  Copy full SHA for 09530bd

• implement suggested changes

  Show description for 52da9bb
  mildsunrise

  committed
  52da9bb

  Copy full SHA for 52da9bb