diff --git a/core/src/sphinx/imperative.rst b/core/src/sphinx/imperative.rst index 96ed4f70..2ebf4f11 100644 --- a/core/src/sphinx/imperative.rst +++ b/core/src/sphinx/imperative.rst @@ -10,6 +10,8 @@ On the technical side, these extensions do not have specific treatment in the back-end of Stainless. Instead, they are desugared into :doc:`Pure Scala ` constructs during a preprocessing phase in the Stainless front-end. +These transformations are partly documented in the `EPFL PhD thesis of Regis Blanc `_. + Imperative Code ---------------