*To*: Walther Neuper <wneuper at ist.tugraz.at>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] value gcd*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 29 Sep 2015 11:53:56 +0200*In-reply-to*: <560A5AFF.4070608@ist.tugraz.at>*References*: <560A5AFF.4070608@ist.tugraz.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

Dear Walther,

You can find out what is happening by inspecting the code equations for gcd with the command code_thms gcd You will see that there are not equations registered. Best, Andreas On 29/09/15 11:33, Walther Neuper wrote:

Given ... theory Demo imports Main begin function gcd :: "int => int => int" where "gcd m n = (if n = 0 then m else gcd n (m mod n))" by auto value "5 mod 3::int" --{*evaluates to "2" :: "int"*} value "gcd 123456 7890::int" --{*evaluates to "Demo.gcd 123456 7890" :: "int"*} end ... why does "gcd" not evaluate, although "mod" evaluates? Walther PS: And how find an answer to such a question myself?

**References**:**[isabelle] value gcd***From:*Walther Neuper

- Previous by Date: Re: [isabelle] Retriving induction scheme for datatype
- Next by Date: [isabelle] A fast implementation of concat for strings?
- Previous by Thread: [isabelle] value gcd
- Next by Thread: [isabelle] A fast implementation of concat for strings?
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list