Skip to content

[ fix ] issue #2905#2927

Merged
JacquesCarette merged 2 commits intoagda:masterfrom
jamesmckinna:inline-vec-functional
Feb 3, 2026
Merged

[ fix ] issue #2905#2927
JacquesCarette merged 2 commits intoagda:masterfrom
jamesmckinna:inline-vec-functional

Conversation

@jamesmckinna
Copy link
Copy Markdown
Collaborator

@jamesmckinna jamesmckinna commented Jan 30, 2026

Only outstanding questions in my mind:

  • (possibly PR-creep for this one) should we also inline the other aliases for Function.Base operations, eg _⊛_ in Data.Vec.Functional?
  • (possible downstream PR) should we, as policy, allow/mandate 'hereditary inlining' for such definitions in general? (eg. the INLINE specialised operations in Tactic.RingSolver.Reasoning could arguably be applied to their definitions in Algebra.Structures, etc. and hence make the former obsolete?)

@jamesmckinna jamesmckinna linked an issue Jan 30, 2026 that may be closed by this pull request
@JacquesCarette JacquesCarette added this pull request to the merge queue Feb 3, 2026
Merged via the queue into agda:master with commit 18055fb Feb 3, 2026
12 checks passed
@jamesmckinna
Copy link
Copy Markdown
Collaborator Author

Thanks @JacquesCarette : any thoughts on subsequent inlinings in this module, or elsewhere?

@JacquesCarette
Copy link
Copy Markdown
Collaborator

I think we should be sparing with our inlinings, and do them when someone actively notices that it is a hindrance.

plt-amy pushed a commit that referenced this pull request Feb 9, 2026
* [ fix ] issue #2905

* fix: words
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.

Inline Data.Vec.Functional.map for Better Termination Checking

3 participants