deep recursion error reducing strings

Stream: new members

[Kevin Sullivan]

I'm wondering why using #reduce to evaluate even one-character strings leads to a stack overflow in the default configuration of Lean? To replicate, try this.

#reduce "-"

[Rob Lewis]

A string is a list of chars. A char is a pair of a nat n and a proof of n < 55296 ∨ 57343 < n ∧ n < 1114112. The normal form of that proof is very very large.

[Gabriel Ebner]

Already the numbers that Rob posted are huge when you unfold them completely:

#reduce 15153 -- works
#reduce 15154 -- stack overflow

[Kevin Sullivan]

I see. Ok. For pedagogy, this is inconvenient, as reduce doesn't work to show terms involving strings and #eval prints them in kernel rather than source format. But it is what it is, and I understand there's no workaround. Thank you, gentlemen.

Gabriel Ebner said:

Already the numbers that Rob posted are huge when you unfold them completely:

#reduce 15153 -- works
#reduce 15154 -- stack overflow

[Rob Lewis]

#eval prints them in kernel rather than source format

Not sure exactly what you mean by this, but do you want #eval repr "-"? (Same on that example, but compare with something with new lines or whatever.)