From e7b8a514507c67bfca36604bb1fd0390942cee09 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 6 Jan 2025 17:47:02 -0800 Subject: [PATCH] Generate base construtors for inductives with univ params. --- src/smtencoding/FStarC.SMTEncoding.Encode.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index aaff2f69b9f..64defc86709 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Encode.fst @@ -1346,7 +1346,7 @@ let encode_datacon (env:env_t) (se:sigelt) constr_fields=univ_fields@fields; constr_sort=Term_sort; constr_id=Some (varops.next_id()); - constr_base=not injective_type_params + constr_base=not injective_type_params || not (List.isEmpty univ_fields); } |> Term.constructor_to_decl (Ident.range_of_lid d) in let app = mk_Apply ddtok_tm vars in let guard = mk_and_l guards in