I’m afraid it depends.
There are at least three different options.
The obvious one is to use an option type in the range. This makes everything
very explicit, but can be quite ugly.
Another approach is to just use the normal function space, knowing that you
will have the intended domain provided “at some distance”. For example, define
a monoid type:
<| carrier : α set; opn : α -> α -> α; id: α |>
The third approach would more explicitly tie the domain into the type
representing the function value so that you might write
type_abbrev (“fn”, ``:(α -> β) # (α set)``)
If manipulating such values, you’d end up wanting to define what it means to
apply these, to compose them etc. I don’t know of any serious attempts to
follow this sort of approach through.
Michael
On 6/12/17, 08:59, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote:
Hello.
Is there some established standard as to how to represent a function
with a domain that may be smaller than the type? More specifically, I
need a representation of arbitrary products (i.e.: The “tuples” are
functions from an arbitrary set to the elements of the tuple) to
formalize theorems about product spaces in topology.
If there does not exists a suitable existing formalization, I have no
problem writing it myself, but it would be good to re-use existing work
to avoid wasted time and to have better integration with other (possibly
future) HOL theories that use functions with explicit domain and
products of an arbitrary “indexed collection” of sets.
Thanks.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
