Re: [Ur] expressing non-emptiness?

2017-05-10 Thread 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.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


[Ur] expressing non-emptiness?

2017-05-10 Thread Marko Schuetz-Schmuck
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.

Best regards,

Marko


signature.asc
Description: PGP signature
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur