diff options
| author | Son HO | 2022-09-22 16:26:58 +0200 |
|---|---|---|
| committer | GitHub | 2022-09-22 16:26:58 +0200 |
| commit | 763e4e641f2dc349bee1820d2c5e4310fc2f07fa (patch) | |
| tree | 4fdb4466206ae8d54ba2f1dced5152150e9ff542 | |
| parent | f76262172b1331c2e3b4d27bce777f30c0ca7967 (diff) | |
Update src/ExtractToFStar.ml
Diffstat (limited to '')
| -rw-r--r-- | src/ExtractToFStar.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 29203bc4..059a7f2e 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1547,7 +1547,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) However, generate its body separately from its declaration to extract the result value. For example, - `let x = 3` + `static X: u32 = 3;` will be translated to `let x_body : result int = Return 3` |