Zulip Chat Archive

Stream: new members

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


view this post on Zulip Scott Morrison (Mar 05 2019 at 23:17):

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

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:17):

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

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:17):

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

view this post on Zulip Simon Hudon (Mar 05 2019 at 23:17):

That sounds like something that should exist in tactic.basic

view this post on Zulip Simon Hudon (Mar 05 2019 at 23:18):

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

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:19):

name.is_internal?

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:21):

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

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:21):

I'll experiment, instead.

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:21):

I think it's exactly what you said

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:21):

Great.

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:22):

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

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:22):

you should probably not go via components like that

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:23):

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

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:24):

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

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:24):

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

view this post on Zulip Simon Hudon (Mar 05 2019 at 23:25):

head

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:28):

What is name.mk_numeral, anyway?

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:32):

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

view this post on Zulip Scott Morrison (Mar 05 2019 at 23:34):

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

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:34):

no, I think it's literally what you said

view this post on Zulip Mario Carneiro (Mar 05 2019 at 23:34):

it just checks for an initial underscore


Last updated: May 08 2021 at 03:17 UTC