Wrapping Up and Documenting LAMBDA++
In this lesson we wrap up and nicely document LAMBDA++. In doing so, we also take the freedom to reorganize the semantics a bit, to make it look better.
See the lambda.k file, which is self-explanatory.
Part 3 of the tutorial is now complete. Part 4 will teach you more features of the K framework, in particular how to exhaustively explore the behaviors of non-deterministic or concurrent programs.