Skip to content

Add family_uncurry_after_ lemmas for the communication primitives #28

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.

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

Open
javierdiaz72 opened this issue Jan 5, 2023 · 2 comments · May be fixed by #29
Open

Add family_uncurry_after_ lemmas for the communication primitives #28

javierdiaz72 opened this issue Jan 5, 2023 · 2 comments · May be fixed by #29

Comments

@javierdiaz72
Copy link

Currently, we have family_uncurry_after_ lemmas for the constructs of the Þ-calculus. We shall extend this configuration to include family_uncurry_after_ lemmas also for the communication language primitives. In addition, we shall add these new lemmas to the built-in list of pre-simplification rules.

@jeltsch
Copy link
Contributor

jeltsch commented Jan 8, 2023

Could you maybe resolve this right now as part of #23? When resolving it, please take care to not introduce an extra lemmas specification for assigning the induct_simp attribute, but assign induct_simp within the lemmas themselves. In the Þ-calculus, it makes sense to have that separate lemmas specification, since making the lemmas in question pre-simplification rules can only be motivated once we have the synchronous transition system defined, while the lemmas themselves appear already in Thorn_Calculus-Foundations and Thorn_Calculus-Processes.

@javierdiaz72
Copy link
Author

Could you maybe resolve this right now as part of #23?

Please note that pushing these changes as part of #23 would make the automated builds fail since we should first merge input-output-hk/thorn-calculus#76 into master. Should I go ahead nevertheless?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants