Failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ
Makarius
makarius at sketis.net
Sun Jan 26 17:28:27 CET 2025
We have a failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ, using
Isabelle/989e661398d6 + AFP/5cb6756ec5b0 and ISABELLE_SMLNJ=/usr/bin/sml in
$ISABELLE_HOME_USER/etc/settings (e.g. with the regular Ubuntu package for smlnj):
/tmp/isabelle-makarius/process8926374598986055100/Code_Test5534440/generated.sml:222.22-223.61
Error: case object and rules don't agree [tycon mismatch]
rule domain: ?.int * int
object: int * int
in expression:
(case ((div_mod k) max_index)
of (b,s) => word_of_int s :: (replicate <exp>) word_max_index)
uncaught exception Error
Makarius
More information about the isabelle-dev
mailing list