Code

Unification#48

Code

Draft

EwenBC wants to merge 34 commits intojespercockx:mainjespercockx/agda-core:mainfrom EwenBC:mainEwenBC/agda-core:mainCopy head branch name to clipboard

+1,069-36

Commits

Commits on Nov 4, 2024

• telescopic equality

  EwenBC

  committed
  ed4c5e1

  Copy full SHA for ed4c5e1

Commits on Nov 5, 2024

• equivalence

  EwenBC

  committed
  89b361f

  Copy full SHA for 89b361f

Commits on Nov 6, 2024

• notations telescope

  EwenBC

  committed
  968ecbf

  Copy full SHA for 968ecbf

Commits on Nov 11, 2024

• solutionL

  EwenBC

  committed
  4cb28e5

  Copy full SHA for 4cb28e5

• fix haskel

  EwenBC

  committed
  4ab5d8b

  Copy full SHA for 4ab5d8b

Commits on Nov 12, 2024

• cut

  EwenBC

  committed
  b101cde

  Copy full SHA for b101cde

• SoltionL with cut

  EwenBC

  committed
  cfcbf44

  Copy full SHA for cfcbf44

• Cleaning code

  EwenBC

  committed
  804fae5

  Copy full SHA for 804fae5

Commits on Nov 20, 2024

• Shrink

  EwenBC

  committed
  a0bb213

  Copy full SHA for a0bb213

Commits on Nov 21, 2024

• Change definition of telescopic equality

  EwenBC

  committed
  4eaa7f2

  Copy full SHA for 4eaa7f2

Commits on Nov 28, 2024

• addTel

  EwenBC

  committed
  3f3e6ed

  Copy full SHA for 3f3e6ed

• Deletion and Injectivity

  Show description for b8de7ec
  EwenBC

  committed
  b8de7ec

  Copy full SHA for b8de7ec

Commits on Nov 29, 2024

• cleaning code

  Show description for 1fbf524
  EwenBC

  committed
  1fbf524

  Copy full SHA for 1fbf524

Commits on Dec 10, 2024

• Dependant Injectivity

  EwenBC

  committed
  aff2a03

  Copy full SHA for aff2a03

Commits on Dec 13, 2024

• Conflict rule

  EwenBC

  committed
  08dbe00

  Copy full SHA for 08dbe00

Commits on Dec 19, 2024

• Changes in Scope library and commented work in progress

  EwenBC

  committed
  7156c9e

  Copy full SHA for 7156c9e

Commits on Jan 6, 2025

• fix haskell (partial)

  EwenBC

  committed
  5a8d716

  Copy full SHA for 5a8d716

Commits on Jan 7, 2025

• bump scopes version

  liesnikov

  committed
  f6fc03c

  Copy full SHA for f6fc03c

• bump scope version again

  liesnikov

  committed
  ba39089

  Copy full SHA for ba39089

• switch to Index instead of In

  Show description for 370a3a2
  liesnikov

  committed
  370a3a2

  Copy full SHA for 370a3a2

Commits on Jan 13, 2025

• swap variables in a context

  EwenBC

  committed
  f04a518

  Copy full SHA for f04a518

Commits on Jan 14, 2025

• Termination of swap function

  EwenBC

  committed
  9981d9c

  Copy full SHA for 9981d9c

• code compartimentation in modules

  EwenBC

  committed
  4cc6c3f

  Copy full SHA for 4cc6c3f

Commits on Jan 22, 2025

• code cleaning

  Show description for a6b8429
  EwenBC

  committed
  a6b8429

  Copy full SHA for a6b8429

• Renaming to Subst

  EwenBC

  committed
  c112cb0

  Copy full SHA for c112cb0

Commits on Jan 23, 2025

• SwapHighest with Renaming

  EwenBC

  committed
  be42b7d

  Copy full SHA for be42b7d

• swap using renaming

  EwenBC

  committed
  0112e50

  Copy full SHA for 0112e50

Commits on Jan 28, 2025

• swapVarList temporary and unsafe version

  EwenBC

  committed
  e606073

  Copy full SHA for e606073

• unsafe swapVarTerm

  EwenBC

  committed
  2e9a73d

  Copy full SHA for 2e9a73d

Commits on Jan 29, 2025

• unsafe swapVarTermStrengthened

  EwenBC

  committed
  169f2b2

  Copy full SHA for 169f2b2

Commits on Jan 31, 2025

• code cleaning, replacing TCM by Maybe in swap and making swapVarTerm safe

  Show description for ed44547
  EwenBC

  committed
  ed44547

  Copy full SHA for ed44547

• removing cases on TCM

  EwenBC

  committed
  490b0a0

  Copy full SHA for 490b0a0

• fuel for swapHighest and a context to try make test

  EwenBC

  committed
  06ee122

  Copy full SHA for 06ee122

Commits on Feb 12, 2025

• Tests for swap highest and minor edits

  EwenBC

  committed
  f0a42b4

  Copy full SHA for f0a42b4