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