Skip to content

Conversation

@gallais
Copy link
Member

@gallais gallais commented Sep 30, 2022

No description provided.

@jamesmckinna
Copy link
Collaborator

Just one query about the type

cast-is-subst : cast eq k ≡ subst Fin eq k

The name of this term (going from left-to-right) is consistent with the other cast-is-* terms.

But to me, the type seems the wrong way round?

If the general aim of equations in the std-lib is to 'reduce complex expressions to simpler', then in this instance, and for all the reasons previously discussed for preferring cast to subst, then shouldn't this equation be oriented from subst in favour of cast?, ie

subst-is-cast : subst Fin eq k ≡ cast eq k

If not, I'd love to be have that spelt out.

Either way, I'm otherwise happy with this PR as it stands.

@JacquesCarette
Copy link
Collaborator

I agree with @jamesmckinna on the 'wanted' direction of that one lemma, and on this otherwise being ready.

@MatthewDaggitt MatthewDaggitt linked an issue Oct 4, 2022 that may be closed by this pull request
@MatthewDaggitt MatthewDaggitt merged commit a123840 into agda:master Oct 4, 2022
jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this pull request Oct 4, 2022
@gallais gallais deleted the fin-cast branch October 4, 2022 14:44
@andreasabel andreasabel mentioned this pull request Aug 27, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Missing cast properties

4 participants