On 10/08/2021 17:34, Florian Haftmann wrote:
> Dear power users of the bit and word libraries,
>
> I have finished polishing the bit and word material as envisaged before
> the next Isabelle release.
Is this failure a consequence of it? (Seen in current Isabelle/0f051404f487 +
AFP/bd6c4c7c76ec)
Native_Word FAILED
(see also
/Users/wenzelm/.isabelle/heaps/polyml-5.8.2_x86_64_32-darwin/log/Native_Word)
*** Type unification failed: Clash of types "_ ⇒ _" and "uint64"
***
*** Type error in application: operator not of function type
***
*** Operator: x :: uint64
*** Operand: AND :: ??'a
***
*** At command "lemma" (line 25 of "$AFP/Native_Word/Native_Word_Test_GHC.thy")
*** At command "test_code" (line 13 of
"$AFP/Native_Word/Native_Word_Test_GHC.thy")
*** Type unification failed: Clash of types "_ ⇒ _" and "uint64"
***
*** Type error in application: operator not of function type
***
*** Operator: x :: uint64
*** Operand: AND :: ??'a
***
*** At command "lemma" (line 25 of "$AFP/Native_Word/Native_Word_Test_GHC.thy")
Unfinished session(s): Native_Word
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
