New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added cong and map to vec ≋ equality #1956

Merged

MatthewDaggitt merged 11 commits into agda:master from guilhermehas:relation-vec-funcs

Jun 15, 2023

Contributor

guilhermehas commented Apr 29, 2023

I added these functions to the file Data.Vec.Relation.Binary.Equality.Setoid:

  cong-[]≔ : i p → xs ≋ ys → xs [ i ]≔ p ≋ ys [ i ]≔ p
  map-[]≔ : i (f : B → A) (xs : Vec B n) p → map f xs [ i ]≔ f p ≋ map f (xs [ i ]≔ p)


          Added cong and map to vec equality

667eff9

jamesmckinna reviewed

View reviewed changes

CHANGELOG.md Outdated Show resolved Hide resolved

jamesmckinna reviewed

View reviewed changes

CHANGELOG.md Outdated Show resolved Hide resolved

jamesmckinna reviewed

View reviewed changes

src/Data/Vec/Relation/Binary/Equality/Setoid.agda Outdated Show resolved Hide resolved

jamesmckinna reviewed

View reviewed changes

src/Data/Vec/Relation/Binary/Equality/Setoid.agda Outdated Show resolved Hide resolved

jamesmckinna reviewed

View reviewed changes

src/Data/Vec/Relation/Binary/Equality/Setoid.agda Outdated Show resolved Hide resolved

guilhermehas added 5 commits

April 29, 2023 15:25


          fixed some mistakes

0098d67


          removec cong from setoid to pointwise

f6ed5a2


          changed order of map f []:==

0ea6df3


          made the code cleaner

42604fa


          changed the location of ->

fd5a584

MatthewDaggitt reviewed

View reviewed changes

Contributor

MatthewDaggitt left a comment

Other than that, looks good to me.

src/Data/Vec/Relation/Binary/Equality/Setoid.agda Outdated Show resolved Hide resolved

MatthewDaggitt added this to the v2.0 milestone

MatthewDaggitt added addition status: being-worked-on labels


          improved identation

2baac45

guilhermehas requested a review from MatthewDaggitt

May 6, 2023 19:05

gallais approved these changes

View reviewed changes

src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda Outdated Show resolved Hide resolved


          renamed concat to cong

gallais reviewed

View reviewed changes

src/Data/Vec/Relation/Binary/Equality/Setoid.agda Outdated Show resolved Hide resolved

src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda Outdated Show resolved Hide resolved

guilhermehas and others added 3 commits

May 13, 2023 14:21


          Update spaces in map-[]≔

e6069ae

Co-authored-by: G. Allais <[email protected]>


          Update spaces in cong-[_]≔

53270ac

Co-authored-by: G. Allais <[email protected]>


          Merge branch 'master' into relation-vec-funcs

e266443

MatthewDaggitt added status: ready and removed status: being-worked-on labels

MatthewDaggitt merged commit 4fe9439 into agda:master

plt-amy pushed a commit that referenced this pull request


          Added cong and map to vec ≋ equality (#1956)

28a739a

andreasabel mentioned this pull request

Put indexed data types in the right universes #2030

Merged

andreasabel mentioned this pull request

Merged

andreasabel mentioned this pull request

Bump Haskell CI (fork) to latest GHC versions #2142

Closed

MatthewDaggitt pushed a commit that referenced this pull request


          Added cong and map to vec ≋ equality (#1956)

029556f

andreasabel pushed a commit that referenced this pull request


          Added cong and map to vec ≋ equality (#1956)

d3e8a84

andreasabel mentioned this pull request

agda pr 7349 #2441

Closed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels