[isabelle] Upt y upto



Dear all,

in the file List.thy there are two definitions of list intervals;

The first one is meant to work with the natural numbers (ihe list of
natural numbers greater or equal than a given "i" and strictly smaller
than a given one):

primrec
  upt :: "nat => nat => nat list" ("(1[_..</_'])") where
    upt_0: "[i..<0] = []"
  | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"

The second one, over the integers (every integer between some given
"i" and "j"):

function upto :: "int => int => int list" ("(1[_../_])") where
"upto i j = (if i ≤ j then i # [i+1..j] else [])"
by auto
termination
by(relation "measure(%(i::int,j). nat(j - i + 1))") auto

Is there any good reason why upt is not extended to the "int" type,
and upto to the "nat" type?

Thanks for the info,

Jesus

-- 
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España





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