Skip to content

Conversation

@oskgo
Copy link
Contributor

@oskgo oskgo commented Nov 13, 2025

Fixes #55.

remove unneccessary argument in PRG example
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull Request Overview

This PR fixes issue #55 by adding validation to detect when bijection arguments are provided to sided rnd operations but would be unused, emitting a type check error instead of silently ignoring them.

Key Changes:

  • Modified pattern matching in t_equiv_rnd_r to check bij_info parameter when processing sided rnd operations
  • Updated example code to remove unused predT argument from rnd{2} call

Reviewed Changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File Description
src/phl/ecPhlRnd.ml Enhanced pattern matching to validate that bijection info is absent ((None, None)) when using sided rnd, otherwise emit "invalid argument" error
examples/PRG.ec Removed unused predT argument from rnd{2} call that is now correctly flagged as an error by the type checker

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@fdupress
Copy link
Member

@oskgo Without looking at the code, and taking only Copilot's review into account, here: is there any chance we can do better than "invalid argument" as an error message? (Not for this release, since this is potentially a breaking change, but merging ASAP after release would be good.)

@oskgo
Copy link
Contributor Author

oskgo commented Nov 15, 2025

@fdupress We could, yes. I'm currently just constraining the pattern matching, otherwise letting it fall through to the existing error message. The error messages for the existing errors could probably use some work too.

@strub strub self-assigned this Nov 18, 2025
@strub strub merged commit 3ee0c81 into main Nov 18, 2025
15 checks passed
@strub strub deleted the fix-55 branch November 18, 2025 15:06
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.

when rnd{1} and rnd{2} are given arguments, an error message is needed

4 participants