Conversation
|
Not urgent, but please fix the title of the PR at some point to start with the required |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
This looks much better! The theory now all lines up, there are some additional small style/technical issues I have pointed out below. Please also see the failures in CI now that it has made it to the linting step.
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
| We first define what is denoted Tran* in [WinskelNielsen1995]: the extension of | ||
| a transition relation with idle transitions. | ||
| -/ | ||
| def lift (trans : State → Label → State → Prop) : State → (Option Label) → State → Prop := |
There was a problem hiding this comment.
This is currently named Cslib.lift, which still isn't a great name/location combo. I'd say LTS.lift, except this is unbundled which makes that an odd name. Deferring to @fmontesi on this.
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Please see my naming comment above, but otherwise things look in pretty good shape to me.
(I pushed a few small commits, the most important of which is probably using some API from Mathlib.Control instead of breaking down notation with change)
4 participants
This PR resolves #387.