Skip to content

Conversation

@Alizter
Copy link
Collaborator

@Alizter Alizter commented May 13, 2024

This commit is from #1929. I ended up using this elsewhere outside of #1929 so I deemed it was of interest on its own.

<!-- ps-id: 2e5b6749-fcba-4dad-aa18-02241cc5007d -->
@Alizter Alizter requested a review from jdchristensen May 13, 2024 23:53
This was referenced May 14, 2024
@Alizter Alizter merged commit 2f00047 into HoTT:master May 17, 2024
@Alizter Alizter deleted the ps/rr/abstract_out_some_idioms_for_dealing_with_decidable_types branch May 17, 2024 20:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants