# Re: [isabelle] Exception Chr raised while processing "fun" (Isabelle 2016)

Hi Eugene,

`The problem seems to be with lexicographic_order (it probably tries to generate some error
``or info message in which a conversion to characters fails). If you use size_change in the
``termination proof, it works:
`
function (sequential) F :: "'a term â int"
where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
| "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
| "F (T (U, b)) = 1 + F b"
| "F (T (a, U)) = 1 + F a"
| "F (T (a, b)) = (F a) + (F b)"
| "F a = undefined"
by pat_completeness auto
termination by size_change
Best,
Andreas
On 17/10/16 12:17, Eugene W. Stark wrote:

Any ideas about the following?
theory Barf
imports Main
begin
datatype 't "term" =
Const 't
| U
| T "'t term * 't term"
| C "'t term * 't term"
| L "'t term"
| L' "'t term"
| R "'t term"
| R' "'t term"
| A "'t term * 't term * 't term"
| A' "'t term * 't term * 't term"
fun F :: "'a term â int"
where "F (T (T (U, b), c)) = 1 + F (T (U, T (b, c)))"
| "F (T (T (a, b), c)) = 1 + F a + F (T (b, c))"
| "F (T (U, b)) = 1 + F b"
| "F (T (a, U)) = 1 + F a"
| "F (T (a, b)) = (F a) + (F b)"
| "F a = undefined"
(* exception Chr raised (line 268 of "./basis/String.sml") *)
end

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