From fc11e50e6954108994c910aa0a26fc6579168fcf Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sat, 5 Oct 2024 00:37:07 +0100 Subject: [PATCH] cv translator: allow known fun types in ctors --- src/num/theories/cv_compute/automation/cv_typeLib.sml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/num/theories/cv_compute/automation/cv_typeLib.sml b/src/num/theories/cv_compute/automation/cv_typeLib.sml index 43125cc806..2d6a3143d5 100644 --- a/src/num/theories/cv_compute/automation/cv_typeLib.sml +++ b/src/num/theories/cv_compute/automation/cv_typeLib.sml @@ -429,7 +429,10 @@ fun define_from_to_aux ignore_tyvars ty = (* val cons_tm = hd conses *) fun check_for_fun_ty cons_tm = let val cons_tys = cons_tm |> type_of |> strip_fun_ty - val bad_tys = filter contains_fun_ty cons_tys + fun not_supported ty = (from_to_for tyvars_alist ty; false) + handle Missing_from_to _ => true + fun is_bad ty = not_supported ty andalso contains_fun_ty ty + val bad_tys = filter is_bad cons_tys in if null bad_tys then () else let