[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Tue, 14 Jun 2016 16:29:26 +0200*References*: <c9f9a016-fcd1-4d87-abc0-1b594b6455f0@googlegroups.com> <FEFF636D-58CE-42CF-AC5D-A01D63E11D45@gmail.com> <de4b10c7-87c0-4a96-bf3e-0727c2a8bb9f@googlegroups.com>

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 ] that help you reduce DOMAIN f to a specific set. Stephan |

**Follow-Ups**:**Re: [tlaplus] Function domains in TLAPS***From:*Ron Pressler

**References**:**Function domains in TLAPS***From:*Ron Pressler

**Re: [tlaplus] Function domains in TLAPS***From:*Stephan Merz

**Re: [tlaplus] Function domains in TLAPS***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] Function domains in TLAPS** - Next by Date:
**Re: [tlaplus] Function domains in TLAPS** - Previous by thread:
**Re: [tlaplus] Function domains in TLAPS** - Next by thread:
**Re: [tlaplus] Function domains in TLAPS** - Index(es):