Re: [isabelle] formalising abstract machines



>> Would it be better to simply make an infinite recursive call as a last pattern?
>> 
>> | abstract_machine arguments = abstract_machine arguments
>> 
>> letting it not to terminate at all?

> You would not be able to define this with "fun" and would need to use 
> "partial_function (option)". However, you should only do this if it is a 
> genuine case of nontermination and not failed pattern-matching turned 
> into artificial nontermination.
>
> Tobias

Where can I find documentation on this `partial_function (option)` keyword? I did not find it in the function definition paper -- I have found its definition in an ML file but that was not very helpful.

- Gergely




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.