*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] value gcd*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Tue, 29 Sep 2015 11:33:51 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

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?

**Follow-Ups**:**Re: [isabelle] value gcd***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Retriving induction scheme for datatype
- Next by Date: Re: [isabelle] Retriving induction scheme for datatype
- Previous by Thread: Re: [isabelle] Retriving induction scheme for datatype
- Next by Thread: Re: [isabelle] value gcd
- 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