We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent e707306 commit dbafe1fCopy full SHA for dbafe1f
tests/lean/run/iterators.lean
@@ -41,7 +41,6 @@ section WellFoundedRecursion
41
def sum (l : List Nat) : Nat :=
42
go l.iter 0
43
where
44
- @[specialize] -- The old code generator seems to need this.
45
go it acc :=
46
match it.step with
47
| .yield it' out _ => go it' (acc + out)
@@ -71,7 +70,6 @@ section Take
71
70
def sumTakeRec (l : List Nat) : Nat :=
72
go (l.iter.take 2) 0
73
74
75
76
77
0 commit comments