startswith

Stream: general

[Patrick Massot]

Do we have something like string.startswith : string -> string -> bool somewhere?

[Mario Carneiro]

There are <:+ and <+: for comparing lists, you could use that

[Gabriel Ebner]

Omg. Did you get these hieroglyphs from Haskell or from Scala?

[Patrick Massot]

I currently use

def string.startswith (s s' : string) : Prop := (s'.to_list).is_prefix_of s.to_list

instance (s s') : decidable (string.startswith s s') :=
by unfold string.startswith ; apply_instance

[Patrick Massot]

I guess one of your hieroglyphs stands for list.is_prefix_of

[Patrick Massot]

But my hope was really that all this should be there already

[Mario Carneiro]

the hieroglyphs were a terrible idea that I now regret

[Mario Carneiro]

I agree that we should have this function already defined. In particular, you can make a more efficient implementation by working with string iterators instead of lists

[Mario Carneiro]

I should load up the docs for strings in haskell or java and copy everything I see

[Patrick Massot]

I vote for doing that as soon as all topology and commutative algebra PR will be merged!

[Mario Carneiro]

I'm working on #464, making good progress

[Mario Carneiro]

what commutative algebra PRs?

[Patrick Massot]

I'm joking, keep going on analysis. You'll have many nights in Amsterdam for algebra

[Sebastien Gouezel]

I'm working on #464, making good progress

Btw, I updated the PR two days ago, but if you started working on the previous version you can of course disregard the modifications I made.

[Mario Carneiro]

yeah, I noticed and have already incorporated your changes