diff options
| -rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
| -rw-r--r-- | tests/lean/Arrays.lean | 4 | ||||
| -rw-r--r-- | tests/lean/Demo/Properties.lean | 4 | ||||
| -rw-r--r-- | tests/lean/Tutorial.lean | 22 |
4 files changed, 15 insertions, 17 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 8fe36d5b..4aac270f 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1016,8 +1016,6 @@ let keywords () = "where"; "with"; ] - @ (* This comes from the scalar notations: `1u32`, etc. *) - List.map StringUtils.lowercase_first_letter all_int_names | HOL4 -> [ "Axiom"; diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 5f50e580..70b4a26b 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -266,9 +266,9 @@ def index_all : Result U32 := let (s1, to_slice_mut_back) ← Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (i7, s2) ← index_mut_slice_u32_0 s1 - let i9 ← i6 + i7 + let i8 ← i6 + i7 let _ ← to_slice_mut_back s2 - Result.ok i9 + Result.ok i8 /- [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/ diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index 67023727..abdc2985 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp_all; scalar_tac | CCons hd tl => simp_all - if hi: i = 0u32 then + if hi: i = 0#u32 then simp_all else simp_all @@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] - if hx : x = 0i32 then + if hx : x = 0#i32 then simp_all else simp_all diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean index 7d347277..94b70991 100644 --- a/tests/lean/Tutorial.lean +++ b/tests/lean/Tutorial.lean @@ -17,7 +17,7 @@ namespace Tutorial def mul2_add1 (x : U32) : Result U32 := do let x1 ← x + x - let x2 ← x1 + 1u32 + let x2 ← x1 + 1#u32 ok x2 /- There are several things to note. @@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do Because Rust programs manipulate machine integers which occupy a fixed size in memory, we model integers by using types like [U32], which is the type of integers which take their values between 0 and 2^32 - 1 (inclusive). - [1u32] is simply the constant 1 (seen as a [U32]). + [1#u32] is simply the constant 1 (seen as a [U32]). You can see a definition or its type by using the [#print] and [#check] commands. It is also possible to jump to definitions (right-click + "Go to Definition" @@ -229,10 +229,10 @@ open CList divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CCons x tl => - if i = 0u32 + if i = 0#u32 then ok x else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth T tl i1 | CNil => fail Error.panic @@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp only [] -- Perform a case disjunction on [i]. -- The notation [hi : ...] allows us to introduce an assumption in the - -- context, to remember the fact that in the branches we have [i = 0u32] - -- and [¬ i = 0u32]. - if hi: i = 0u32 then + -- context, to remember the fact that in the branches we have [i = 0#u32] + -- and [¬ i = 0#u32]. + if hi: i = 0#u32 then -- We can finish the proof simply by using the simplifier. -- We decompose the proof into several calls on purpose, so that it is -- easier to understand what is going on. @@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) annotates it with the [divergent] keyword. -/ divergent def i32_id (x : I32) : Result I32 := - if x = 0i32 then ok 0i32 + if x = 0#i32 then ok 0#i32 else do - let x1 ← x - 1i32 + let x1 ← x - 1#i32 let x2 ← i32_id x1 - x2 + 1i32 + x2 + 1#i32 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] - if hx : x = 0i32 then + if hx : x = 0#i32 then simp_all else simp [hx] |