Workaround for stack overflows with `has_reflect string` #

The default has_reflect string instance in Lean only work for strings up to few thousand characters. Anything larger than that will trigger a stack overflow because the string is represented as a very deeply nested expression: https://github.com/leanprover-community/lean/issues/144

This file adds a higher-priority instance for has_reflect string, which behaves exactly the same for small strings (up to 256 characters). Larger strings are carefully converted into a call to string.join.

source

meta def string.to_chunks (size : ℕ) :

string → (list string := list.nil) → list string

Splits a string into chunks of at most size characters.

source

@[protected, instance]

meta def thunk.has_reflect {α : Type u_1} [has_reflect α] :

has_reflect (thunk α)

source

@[protected, instance]

meta def string.has_reflect :

has_reflect string

Workaround for stack overflows with has_reflect string #

Workaround for stack overflows with `has_reflect string` #