如何为 `int list` z3 adt dotnet api 定义 adt 构造函数

Question

如何为

int list

定义adt构造函数

Context.MkConstructor(name: string, recognizer: string, ?fieldNames: string array, ?sorts: Sort array, ?sortRefs: uint32 array) : Constructor

文档说（

https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_context.html#a2a421919ab766bf028ec422723b42e37

） "sorts 字段排序，如果字段排序指的是递归，则为 0 sortRefs 对作为构造函数参数的数据类型排序的引用；如果相应的排序引用为 0，则 sort_refs 中的值应该是引用声明的递归数据类型之一的索引。”

_.MkConstructor("cons", "is_cons", [|"x"; "y"|], [|_.mkIntSort (); ?1], ?2)

应该是什么

?

我试着把

?1

设置成

null

，但是我看不懂工作原理

sortRefs

,