[isabelle-dev] fun f where "f 0 = ..." raises TYPE

Tjark Weber webertj at in.tum.de
Thu Mar 17 18:31:42 CET 2011


Hi,

Attempting to define

  fun f where "f 0 = undefined"

in Isabelle/HOL (7f2793d51efc) yields

*** exception TYPE raised (line 38 of
".../isabelle/src/HOL/Tools/Function/pattern_split.ML"): inst_constrs_of
*** At command "fun"

A more user-friendly error message would be nice.

Kind regards,
Tjark




More information about the isabelle-dev mailing list