Re: [isabelle] Sort constraints in the termination relation



sum.cong is a great example, thanks!

Cheers
Lars

On 12 April 2017 16:50:33 CEST, "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at> wrote:
>Hi again,
>
>> 2. To users of the function package: Can you give me an example of a
>> function that uses class axioms to prove termination? Or possibly
>> requires a "fundef_cong" rule with a sort constraint?
>
>looking a bit further, I also found a fundef-cong-rule which contains
>sort-constraints, namely sum.cong.
>
>Look at AFP/Bernoulli/Bernoulli.thy, function bernoulli.
>
>Cheers,
>RenÃ



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