Skip to content

Commit 5fe9499

Browse files
committed
clean up test files
1 parent 9918cd0 commit 5fe9499

File tree

2 files changed

+1
-130
lines changed

2 files changed

+1
-130
lines changed

tests/lean/run/range.lean

Lines changed: 1 addition & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,4 @@
1-
import Init.Data.Range.Polymorphic.Nat
2-
import Init.Data.Range.Polymorphic.Basic
3-
import Init.System.IO
4-
import Init.Data.Iterators
5-
import Std.Data.Iterators
6-
import Init.Data.Range.Polymorphic.Basic
1+
72

83
def ex1 : IO Unit := do
94
IO.println "example 1"
@@ -80,48 +75,3 @@ x: 7
8075
-/
8176
#guard_msgs in
8277
#eval ex4
83-
84-
-- NEW
85-
86-
87-
open Std.Iterators
88-
89-
/-- info: true -/
90-
#guard_msgs in
91-
#eval "b" ∈ ("a"...="c")
92-
93-
/-- info: [1, 2, 3, 4] -/
94-
#guard_msgs in
95-
#eval (1...=4).toList
96-
97-
/-- info: [2, 3] -/
98-
#guard_msgs in
99-
#eval (1<...<4).toList
100-
101-
/-- info: [0, 1, 2, 3, 4] -/
102-
#guard_msgs in
103-
#eval (...=4).toList
104-
105-
/-- info: 2 -/
106-
#guard_msgs in
107-
#eval (1<...<4).size
108-
109-
/-- info: true -/
110-
#guard_msgs in
111-
#eval (1...<1).isEmpty
112-
113-
/-- info: [3, 5, 7, 9, 11, 13] -/
114-
#guard_msgs in
115-
#eval (2<...<15).iter.stepSize 2 |>.toList
116-
117-
/-- info: true -/
118-
#guard_msgs in
119-
#eval 1 ∈ (1...=5)
120-
121-
def g (xs : Array Nat) : Nat := Id.run do
122-
let mut sum := 0
123-
for h : i in (0...<xs.size) do
124-
sum := sum + xs[i]
125-
return sum
126-
127-
#synth ForIn Id (type_of% (2...=8)) _ -- Note that we don't need the type hint this time, but we'd need one in a for loop

tests/lean/run/rangePolymorphic.lean

Lines changed: 0 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -1,85 +1,6 @@
11
import Init.Data.Range.Polymorphic
22
import Std.Data.Iterators
33

4-
def ex1 : IO Unit := do
5-
IO.println "example 1"
6-
for x in [:100:10] do
7-
IO.println s!"x: {x}"
8-
9-
/--
10-
info: example 1
11-
x: 0
12-
x: 10
13-
x: 20
14-
x: 30
15-
x: 40
16-
x: 50
17-
x: 60
18-
x: 70
19-
x: 80
20-
x: 90
21-
-/
22-
#guard_msgs in
23-
#eval ex1
24-
25-
def ex2 : IO Unit := do
26-
IO.println "example 2"
27-
for x in [:10] do
28-
IO.println s!"x: {x}"
29-
30-
/--
31-
info: example 2
32-
x: 0
33-
x: 1
34-
x: 2
35-
x: 3
36-
x: 4
37-
x: 5
38-
x: 6
39-
x: 7
40-
x: 8
41-
x: 9
42-
-/
43-
#guard_msgs in
44-
#eval ex2
45-
46-
def ex3 : IO Unit := do
47-
IO.println "example 3"
48-
for x in [1:10] do
49-
IO.println s!"x: {x}"
50-
51-
/--
52-
info: example 3
53-
x: 1
54-
x: 2
55-
x: 3
56-
x: 4
57-
x: 5
58-
x: 6
59-
x: 7
60-
x: 8
61-
x: 9
62-
-/
63-
#guard_msgs in
64-
#eval ex3
65-
66-
def ex4 : IO Unit := do
67-
IO.println "example 4"
68-
for x in [1:10:3] do
69-
IO.println s!"x: {x}"
70-
71-
/--
72-
info: example 4
73-
x: 1
74-
x: 4
75-
x: 7
76-
-/
77-
#guard_msgs in
78-
#eval ex4
79-
80-
-- NEW
81-
82-
834
open Std.Iterators
845

856
/-- info: true -/

0 commit comments

Comments
 (0)