# Re: [tlaplus] Function domains in TLAPS

On Tuesday, June 14, 2016 at 5:29:29 PM UTC+3, Stephan Merz wrote:

Correct, this is still too unspecific because f[3] denotes some value even if 3 is not an element of the domain of f. I was thinking of assumptions of the kind

f \in [ 0 .. 10 -> Nat ]