如何在Z3中定义较高的归纳类型

Question

较高的归纳类型是同伦类型理论中非常重要的工具。我正在尝试使用Z3-SMT-LIB来定义一些更高级的归纳类型。一个例子是圆圈，由点base和loop，从base到自身的路径自由生成。我使用的代码

(declare-datatypes() ((Circle base (loop (Circle Circle))))) 
(declare-fun x1() Circle) 
(declare-fun x2() Circle) 
(assert (not (= x1 x2))) 
(check-sat) 
(get-model) 

和输出

sat 
(model 
(define-fun x2() Circle (loop base)) 
(define-fun x1() Circle base)) 

的问题是：我真的定义一个名为圆较高感应式？

Answer 1

请注意，Z3仅支持一阶归纳类型。你提供的也是一阶。