diff options
| author | Son Ho | 2024-03-20 06:17:41 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-20 06:17:41 +0100 |
| commit | 5e99d127e0a746f5779779756fccf79f15c19d10 (patch) | |
| tree | 6d10d613179568346e19cbc6bf95c6dd6897f574 /tests/lean/Demo | |
| parent | e6f002cfc1dfa41362bbb3a005c4261d09c52c58 (diff) | |
Regenerate the code
Diffstat (limited to 'tests/lean/Demo')
| -rw-r--r-- | tests/lean/Demo/Demo.lean | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 09032820..4acc69c8 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -40,9 +40,9 @@ def incr (x : U32) : Result U32 := Source: 'src/demo.rs', lines 25:0-25:17 -/ def use_incr : Result Unit := do - let i ← incr 0#u32 - let i1 ← incr i - let _ ← incr i1 + let x ← incr 0#u32 + let x1 ← incr x + let _ ← incr x1 Result.ret () /- [demo::CList] |