我想知道,是否有可能不按类型递归地定义其值相互依赖的记录?method n : a -> a -> Baz
其中n足够大,我想把所有这些都打包成记录,而不是仅仅有一堆相互递归的函数。(而且,我使用SomeRec作为实例参数)。值得注意的是,SomeRec不是递归的:它的字段类型中没有一个引用SomeRec。原则上可以
我知道Coq允许定义相互递归的归纳类型。但是有没有一种方法可以用Coq编写递归定义呢?例如,我想将一个定义写为:
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).上述定义中的重要部分是myDefinition B,它在另一个参数上递归调用相同<em