Add 'missing' price functions for hml_srbb*

equivio / silent-step-spectroscopy

Isabelle formalization of linear-time–branching-time spectroscopy accounting for silent steps

https://equivio.github.io/silent-step-spectroscopy/AFP/LinearTimeBranchingTimeSpectroscopyAccountingForSilentSteps/index.html

Other

0 stars 0 forks source link

Add 'missing' price functions for hml_srbb* #79

Closed TheHllm closed 10 months ago

TheHllm commented 10 months ago

Some of the pricing functions are 'missing' from main and have already been added in different branches. These changes should pushed to main and merged back into the branches that already added these definitions.

An example of such a price can be found in https://github.com/equivio/silent-step-spectroscopy/blob/ffc48c251c6321e30cb01793c1992f3d7712939b/Expressiveness_Price.thy#L222

betawave commented 10 months ago

Why is this still open if the PR (https://github.com/equivio/silent-step-spectroscopy/pull/81) as been merged?

TheHllm commented 10 months ago

Most likely because it was not linked. I will just close this.