New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Hol_datatype ignores theory indications #257

Closed
xrchz opened this Issue May 25, 2015 · 0 comments

Comments

Projects
None yet
1 participant
@xrchz
Copy link
Member

xrchz commented May 25, 2015

The following session (in theory Scratch) should not fail. It looks like the wrong datatype was defined, making scratch$num recursive when it was explicitly annotated not to be.

> val _ = Datatype`num = Foo (num$num) | Bar`;
<<HOL message: Defined type: "num">>
> ``Foo 0``;
at line 7, character 6: No possible type for overloaded constant _ inject_number
Wanted it to have type:  :num -> num
Exception-
   HOL_ERR
  {message =
  "at line 7, character 6:\nNo possible type for overloaded constant _ inject_number\n",
  origin_function = "typecheck", origin_structure = "Preterm"} raised
> dest_thy_type(fst(dom_rng(type_of``Foo``)));
val it = {Args = [], Thy = "scratch", Tyop = "num"}:
   {Args: hol_type list, Thy: string, Tyop: string}

@xrchz xrchz added the Bug label May 25, 2015

@xrchz xrchz referenced this issue May 25, 2015

Closed

Datatype diverges #258

@mn200 mn200 closed this in 1e90aa9 May 25, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment