summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/ExtractBase.ml2
-rw-r--r--tests/lean/Arrays.lean4
-rw-r--r--tests/lean/Demo/Properties.lean4
-rw-r--r--tests/lean/Tutorial.lean22
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]