Support for FunAsSeq + HOWTO on type annotations #571
Conversation
| - [Supported Features](./apalache/features.md) | ||
| - [TLA+ Preprocessing](./apalache/preprocessing.md) | ||
| - [Fine Tuning](./apalache/tuning.md) | ||
| - [KerA: kernel logic of actions](./apalache/kera.md) | ||
| - [Assignments in Apalache](./apalache/assignments.md) | ||
|
|
||
| # HOWTOs | ||
|
|
||
| - [How to write type annotations](./HOWTOs/howto-write-type-annotations.md) |
There was a problem hiding this comment.
I wonder if this shouldn't just be part of the snowcat sections? Perhaps snowcat needs it's own directory and sub-chapters?
Lots of things int he manual describe how to do things: how to install, how to fine-tune, how to configure. I feel like howto sections often become weird grabbags, and it'd bet cleaner just to structure the manual by topic.
There was a problem hiding this comment.
Right. We have to restructure the docs. The reason why I called it a HOWTO is that I wanted to try this approach: https://documentation.divio.com
There was a problem hiding this comment.
Looking at our current manual, it mixes a tutorial, HOWTOs and explanations. That's why it looks quite weird.
|
|
||
| Consider the example [HourClock.tla][] from [Specifying Systems][]: | ||
|
|
||
| ```tla |
There was a problem hiding this comment.
Should you maybe use the include syntax that we use elsewhere, to ensure that the manual? It helps ensure that the docs will exactly match whatever is in the source file:
There was a problem hiding this comment.
Sure, that's nice. What is 55 here?
There was a problem hiding this comment.
{{#include ../../../test/tla/y2k.tla::55}}
There was a problem hiding this comment.
55 is the line number to start the inclusion from! You can also give a line number to end on. See the mdBook docs for more details :)
Co-authored-by: Shon Feder <[email protected]>
Co-authored-by: Shon Feder <[email protected]>
Followup to #571, which added a link to HOWTOs/index.md but didn't include that page in the summary, resulting in a 404.
This PR closes the issue #223. The type checker now understands the type conversion operator
FunAsSeq. That was quite easy to add, so I diverged in writing the HOWTO on type annotations.The HOWTO is available at: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
make fmt-fix(or had formatting run automatically on all files edited)