Skip to content

Conversation

@andrevidela
Copy link
Collaborator

Description

Prerequisite for #3614

Copy link
Collaborator

@buzden buzden left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then, looks good

@dunhamsteve
Copy link
Collaborator

Looks like a codeberg hiccup, rerunning failed tests.

@dunhamsteve dunhamsteve merged commit a991795 into idris-lang:main Aug 18, 2025
39 of 41 checks passed
@andrevidela andrevidela deleted the impTy-refactor branch August 18, 2025 18:54
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.

3 participants