[Hol-info] HOL-light Exception: Failure "typechecking error (initial type assignment)".

[hao d. <den...@gm...>]

Hello there:
 I have a small piece of code which I don't know where is the problem.


===================================================

let str_IND, str_RECUR = define_type "str = Str (int list)";;

let expr_IND, expr_RECUR = define_type
    " expr = Lit num
            |Var str
            |Plus expr expr
            |Times expr expr ";;

let cmd_IND, cmd_REC = define_type
    "cmd = Assign str expr
            |  Seq cmd cmd
            |  If expr cmd cmd
            |  While expr cmd";;

parse_as_infix(";;", (18, "right"));;
parse_as_infix(":=", (20, "right"));;
override_interface(";;", `Seq`);;
override_interface(":= ", `Assign`);;
override_interface("+", `Plus`);;
override_interface("*", `Times`);;

let value = define
    `(value (Lit n ) s = n )
 /\  (value (Var  x) s = s(x) )
 /\  (value (e + f) s = value e s + value f s )
 /\  (value (e * f) s = value e s * value f s ) `;;

=======================================


Exception: Failure "typechecking error (initial type assignment)".


after that , the system seemed enter an unstable state:



# let fib = define
  `fib n = if n = 0 \/ n = 1 then 1 else fib(n-1) + fib(n-2)`;;
Exception: Failure "typechecking error (initial type assignment)".

any help ?