Skip to content

Conversation

@etiennejf
Copy link
Collaborator

@etiennejf etiennejf commented Nov 20, 2025

Co-domain restriction for undeclared/axiom function and axioms for global lambdas

Description

This PR addresses issue #28 and perform the following modifications:

  • Smt Translation
    • Add co-domain restriction for undeclared class functions or automatized functions
    • Add congruence, extensionality and co-domain restrictions for global lambdas
  • Test suite:
    • Add Issue29.lean to validate that co-domain restriction are properly considered for undeclared/axiom functions.

Closing tickets

Closes #414

Checklist

  • All theorems valid for each formalization in CI
  • All the specified lean file are properly considered when compiling and verifying the formalization
  • Self review of the code has been done.
  • Reviewer has been requested.
  • Reviewer has performed the following tasks
    • Ensure that all the test cases are still valid
    • Ensure that each specified lean file is properly considered in the tool chain.

@etiennejf etiennejf self-assigned this Nov 20, 2025
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.

2 participants