Skip to content

Extension to elaborator reflection interface to enable automated derivation of decidable equality #3779

Open
bhaktishh wants to merge 22 commits into
idris-lang:mainfrom
bhaktishh:main
Open

Extension to elaborator reflection interface to enable automated derivation of decidable equality #3779
bhaktishh wants to merge 22 commits into
idris-lang:mainfrom
bhaktishh:main

Conversation

@bhaktishh
Copy link
Copy Markdown

Description

This PR adds a function to the elaborator reflection interface, to enable automated derivation of decidable equality (in library idris2-elab-util).

The function getDecEqConPairs expects a type, and returns a pair (List Nat, List (String, String)), which represent the indices of the type arguments that are parameters, and pairs of constructor names (as strings) that can have the same type.

For example, for the type Vect, the function would return ([1], [("Nil", "Nil"), ("::", "::")]).

Self-check

  • This is my first time contributing, I've carefully read CONTRIBUTING.md
    and I've updated CONTRIBUTORS with my name.
  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md
  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

@bhaktishh bhaktishh marked this pull request as draft May 19, 2026 14:42
@bhaktishh bhaktishh marked this pull request as ready for review May 19, 2026 14:43
@CodingCellist CodingCellist added enhancement implem: elaboration event: IDM 2026/05 Issue tackled during the May 2026 Idris Developers Meeting labels May 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement event: IDM 2026/05 Issue tackled during the May 2026 Idris Developers Meeting implem: elaboration

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants