Skip to content

replace ImpTy#3615

Merged
dunhamsteve merged 3 commits into
idris-lang:mainfrom
andrevidela:impTy-refactor
Aug 18, 2025
Merged

replace ImpTy#3615
dunhamsteve merged 3 commits into
idris-lang:mainfrom
andrevidela:impTy-refactor

Conversation

@andrevidela
Copy link
Copy Markdown
Collaborator

Description

Prerequisite for #3614

Comment thread src/Core/WithData.idr Outdated
Comment thread src/TTImp/TTImp/TTC.idr
Comment thread src/Core/WithData.idr
Copy link
Copy Markdown
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
Copy Markdown
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