[FOM] partial functions / undefined terms in machine proof

[Freek Wiedijk]

Larry, quoting John:

>[3] Encode the domain of the partial function in its type and make its
>    application to arguments outside that domain a type error.

[3] is my favored approach, but: it does not need to
be linked to types (it is in the proof assistant PVS
<https://en.wikipedia.org/wiki/Prototype_Verification_System>;
is there any serious system that has such type
correctness conditions?)  In the B method proof assistant
<https://en.wikipedia.org/wiki/B-Method> one has approach
[3] too, but there it is not type related.

Freek