[Ur] expressing non-emptiness?

[Adam Chlipala]

No such more refined type of strings is built into Ur/Web, any more than 
it's built into OCaml or Haskell.

On 05/10/2017 06:25 PM, Marko Schuetz-Schmuck wrote:
> I'm puzzled over expressing non-emptiness.
>
> Say, I want to write a function that has a non-empty string
> parameter. How would one express this additional property as some form
> of constraint? Just to be clear, I'm not looking at implementing a new
> type of non-empty strings in parallel to the already existing strings.