You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
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?
Currently, we have
family_uncurry_after_
lemmas for the constructs of the Þ-calculus. We shall extend this configuration to includefamily_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.The text was updated successfully, but these errors were encountered: