Re: [isabelle] recdef woes



While we're about it, the following also fails, generating an
impossible termination condition.  (HOL4 gets this right, Konrad will
be pleased to hear.)

----------------------------------------------------------------------
recdef align_tt "measure size"
  "align_tt char_tt = 1"
  "align_tt short_tt = 2"
  "align_tt int_tt = 4"
  "align_tt long_tt = 4"
  "align_tt ptr_tt = 4"
  "align_tt (array_tt ty n) = align_tt ty"
  "align_tt (struct_tt []) = 0" 
  "align_tt (struct_tt (ty#tys)) = foldr (\<lambda>ty n. max (align_tt ty) n)
                                          tys (align_tt ty)"

----------------------------------------------------------------------

Michael.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.