戰術部分計算目標在勒柯克

quad X Y

，但我不記得了「四」的定義，我不希望啓動其定義的搜索。

有沒有一種策略可以讓我迅速用它的定義代替quad？

Record quad (X Y:Type):= { x:X; y:Y}.

或者我必須記住和使用

refine (@Build_quad _ _).

？

2016-05-31 ged

'constructor' should work is most case。你也可以找到'Hint Constructors'有用。 – ejgallego

順便說一句，在這種情況下搜索是沒有必要的，但它很簡單：'打印quad.'會給你所需的信息。如果您使用的是ProofGeneral，您需要將光標（點）移到感興趣的實體上並點擊「C-c C-a C-p」和「Enter」。 –

你有點誤，Build_quad不是quad的定義，它是它的構造函數。它創建了quad類型的條款。正如@ejgallego所說，你應該在這種情況下使用constructor策略。

您的目標是希望您提供一個類型爲quad X Y的術語，從頭創建這樣一個術語的唯一方法是使用forall X Y: Type, X -> Y -> quad X Y類型的構造函數Build_quad。

2016-06-01 08:45:19 Vinz

爲了完整起見：一個較不自動的方式是'應用Build_quad.'而不是'constructor.' –

通常我使用'split'作爲記錄。 – eponier

回答