search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

No concrete syntax for built-in word types #518

Closed michaelsproul closed 6 years ago

michaelsproul commented 6 years ago

It isn't possible to write a built-in type like word8array in concrete syntax, for example in a datatype definition:

datatype my_type = Cons word8array

As a workaround we're currently under-specifying the type like:

datatype 'a my_type = Cons 'a
SOwens commented 6 years ago

You should be able to. Which commit is your CakeML, and what error message do you get when you try?

michaelsproul commented 6 years ago

Ah, we're using https://github.com/CakeML/cakeml/commit/23cc9570170886049d38a6618b8ba5de610d7082 currently because we rely on derive_eval_thm which was deleted shortly after that. I tried just now with a newer commit (https://github.com/CakeML/cakeml/commit/cd7b362e8c6db50f63d446226a818d237f77f7e5) and it worked fine, so I'll close this issue.

We'll work on updating to master to avoid further trouble (I think Johannes is chatting to Ramana about the derive_eval_thm issue)