VM computation for special characters

Stream: general

[Xin Huajian]

I wrote a simple function to erase specific characters in a string:

meta def erace_curr : string.iterator → char → string.iterator
| ⟨p, c::n⟩ c' := if (c = c') then (erace_curr ⟨p.reverse,n⟩ c') else (erace_curr ⟨c::p.reverse,n⟩ c')
| ⟨p, []⟩   c' := ⟨p, []⟩

#eval string.iterator.prev_to_string $ erace_curr "1234\n567".mk_iterator '\n'

#eval string.iterator.prev_to_string $ erace_curr "α".mk_iterator '\n'

However, while the first #eval sentence returns the right answer "1234567", the second #eval doesn't terminate. Could anyone tell me why and how to fix it? Thanks!

[Floris van Doorn]

I think defining your own functions on string.iterator is not really supported, it is just a data type to interface with string operations written in C++.
You can use something like this:

#eval ("1234\n567".to_list.filter (≠ '\n')).as_string
#eval ("α".to_list.filter (≠ '\n')).as_string

[Xin Huajian]

Floris van Doorn said:

I think defining your own functions on string.iterator is not really supported, it is just a data type to interface with string operations written in C++.
You can use something like this:

#eval ("1234\n567".to_list.filter (≠ '\n')).as_string
#eval ("α".to_list.filter (≠ '\n')).as_string

Thanks! Really elegant!