[isabelle] value gcd



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?




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