Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using Word, Map and Set in Haskabelle

Email Gateway (Aug 18 2022 at 14:31):

From: Andrew Boyton <andrew.boyton@nicta.com.au>
Hi

I have downloaded the latest version of Isabelle, and am trying to use Haskabelle to translate a Haskell file into Isabelle. The Haskell file I am trying to convert imports Data.Word, Data.Map and Data.Set, which I believe should all have Isabelle equivalents, though I am having trouble telling that to Haskabelle. I tried following the instructions in the documentation and adding an adaption for Word, under the "types" section,
"Data.Word.Word" "32 word"
but it still gives the the following error message:
<interactive>: user error (The module "Data.Word" imported from module "Test.Model" cannot be found at "../Data/Word.hs"!)

Any advice on how to get these working would be greatly appreciated.

Thanks
Andrew Boyton

Last updated: Nov 21 2024 at 12:39 UTC