0
如何獲取Coq中所有父元素? 我在Coq的定義一組如下:如何在Coq中表示繼承?
Inductive Gen : Set :=
| BGen : nat -> nat -> Gen.
有許多實例,例如:
Definition g1 = BGen 1 2.
Definition g2 = BGen 2 3.
現在,我想獲得的3父母元件,即[1,2]。我寫一個函數:
Fixpoint parents (c : nat) (l : list Gen) :=
match l with
| [] => []
| (BGen p c') :: l' => if beq_nat c c'
then [p]
else parents c l'
end.
我只能得到直接父的3 [2],我怎樣才能讓所有的家長,如[1,2]在這個例子嗎?
爲什麼如果你找到了匹配而不是返回'p' *而返回'[p]',而且還可以在列表的其餘部分找到其他匹配項? – gallais
@gallais這可以通過用[p] :: parents c l'替換[p]來完成。但是,只有c的父母可以通過使用這個函數找到,我不能得到c的所有父母。 –
啊!看來我誤解了你的目標:你不僅要父母,還要父母的父母等?基本上你想建立一個閉包? – gallais