test if the first character of a string is an underscore?

Stream: new members

[Scott Morrison]

I need to filter a big list of names, discarding all those whose last component starts with an underscore.

[Scott Morrison]

(Throw out all the auto-generated lemmas from the pattern matcher, etc.)

[Scott Morrison]

I can use (to_string n.components.ilast).to_list.head ≠ '_', but apparently on the scale I'm working this is slow.

[Simon Hudon]

That sounds like something that should exist in tactic.basic

[Simon Hudon]

A better way of getting the last component is (name.update_prefix _ n).to_string`

[Mario Carneiro]

name.is_internal?

[Scott Morrison]

I guess I need to read the C++ to find out what name.is_internal actually does. :-)

[Scott Morrison]

I'll experiment, instead.

[Mario Carneiro]

I think it's exactly what you said

[Scott Morrison]

Great.

[Scott Morrison]

Any tricks for throwing out all private names? Currently I just do n.components.head ≠ "_private"

[Mario Carneiro]

you should probably not go via components like that

[Scott Morrison]

Ok. I'll write my own name.is_private by pattern matching?

[Mario Carneiro]

You could define a function for n.components.head and then check that it equals "_private"

[Scott Morrison]

What should the function for n.components.head be called?

[Simon Hudon]

head

[Scott Morrison]

What is name.mk_numeral, anyway?

[Mario Carneiro]

it's an internal thing, you won't see it except in unique names for variables I think

[Scott Morrison]

Are names like cases_on and inj_arrow going to count as internal names?

[Mario Carneiro]

no, I think it's literally what you said

[Mario Carneiro]

it just checks for an initial underscore