Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cv translator: allow known fun types in ctors #1317

Merged
merged 1 commit into from
Oct 9, 2024
Merged

cv translator: allow known fun types in ctors #1317

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion src/num/theories/cv_compute/automation/cv_typeLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down