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 83d23b7 commit d70cfaeCopy full SHA for d70cfae
src/Init/Data/Array/Basic.lean
@@ -2133,5 +2133,3 @@ instance [ToString α] : ToString (Array α) where
2133
toString xs := String.Internal.append "#" (toString xs.toList)
2134
2135
end Array
2136
-
2137
-export Array (mkArray)
0 commit comments