New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

xlp: move parameters in the type #170

Merged

fblanqui merged 3 commits into Deducteam:main from fblanqui:xlp

Feb 1, 2025

Member

fblanqui commented Feb 1, 2025 •

edited

Loading

xlp: move lemma parameters in the type (to be able to turn them into axioms as coq does not accept parameters in axioms)
xlp: in single file generation, prefix theorem names by "thm_" to avoid clashes with term constants

fblanqui added 3 commits

February 1, 2025 21:21


          xlp: move parameters in the type

fa9290b

wip

93be732

wip

45492a9

fblanqui merged commit 7555af5 into Deducteam:main

2 checks passed

fblanqui deleted the xlp branch

February 1, 2025 21:34

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet