[isabelle] Types for Function.get_info



Hi all,

While using "Function.get_info" in Isabelle/HOL(ML), I got an "Empty" 
exception coming from the "the_single" function.

I discovered that when defining a function in Isabelle/HOL, as soon as the 
type variables of the type annotation differs from the ones of the infered 
type (without type annotation), the function is added twice (with these two 
typing informations) to the FunctionData. Then the "the_single" call of 
"Function.get_info" fails (with an Empty exception while the list contains 2 
elements, which can be a little confusing :-)).

Here is a simple example:

----------
fun foo :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b)" where
  "foo a b = (a, b)"

ML {*
  Item_Net.retrieve (Function_Common.get_function @{context}) @{term "foo"}
  |> map #1
*} (* 1 element in the list *)

fun foo' :: "'a \<Rightarrow> 'c \<Rightarrow> ('a * 'c)" where
  "foo' a b = (a, b)"

ML {*
  Item_Net.retrieve (Function_Common.get_function @{context}) @{term "foo'"}
  |> map #1
*} (* 2 elements with similar types in the list *)

ML {* Function.get_info @{context} @{term "foo"} *} (* OK *)
ML {* Function.get_info @{context} @{term "foo'"} *} (* exception Empty *)
----------

Bug or feature ?

Thanks,

Mathieu




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