Re: [isabelle] formalising abstract machines



There is also a page about it in the Isar reference manual:

Isabelle2013-2 doc isar-ref

Section 11.2.2

Dmitriy

Am 30.01.2014 15:51, schrieb Tobias Nipkow:
There are two examples in ex/Fundefs.thy.

Tobias

On 30/01/2014 14:53, Buday Gergely wrote:
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.