Skip to content

Commit 4f70696

Browse files
committed
String.toList semireducible
1 parent 1422c82 commit 4f70696

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/Init/Data/String/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,7 @@ Examples:
237237
* `"".toList = []`
238238
* `"\n".toList = ['\n']`
239239
-/
240-
@[extern "lean_string_data", expose, implicit_reducible]
240+
@[extern "lean_string_data", expose]
241241
def String.toList (s : String) : List Char :=
242242
(String.Internal.toArray s).toList
243243

0 commit comments

Comments
 (0)