[Ur] expressing non-emptiness?

Adam Chlipala adamc at csail.mit.edu
Wed May 10 18:31:49 EDT 2017


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.



More information about the Ur mailing list