如何從已定義的選項中提取具體值

當您撥打mapName(identifier)時，如果返回的內容不是'rangeType option'，並且您確定它是有限映射（有限域和範圍）標識符是否存在於地圖中？如何從已定義的選項中提取具體值

2015-12-17 MooMooCoding

如果你有一個'map_name'類型的''a =>'b選項'並且知道'map_name id'會導致'Some x'對於一些''''''''''''''''''''''可以使用'::'a選項=>'a'來立即提取'x'，即'（map_name x）'將導致'x'。 – chris

這正是我需要的。謝謝你，克里斯！ – MooMooCoding

好的，然後我會將我的評論轉換爲答案，以便將此問題標記爲稍後訪問者的答案。 – chris

在回答你的問題之前，讓我們先說一下我們正在談論的精確的「部分函數」。

（顯式地）在Isabelle/HOL中，部分函數的類型爲'a => 'b option。然後，對於每一個給定x :: 'a這樣的部分功能f :: 'a => 'b option結果無論是在None（意味着f未在x定義）或Some y :: 'b option（每當f實際上x定義）。

現在，如果一些輸入x你知道（這在伊莎貝爾/ HOL應該意味着你有這方面的證據），其f x定義，你可以使用該選項類型的選擇功能the : 'a option => 'a。所以只要f x = Some y然後the (f x)結果在y。

請注意，原則上也可以撥打the None。在這種情況下，我們遇到了Isabelle/HOL中可用的不同類型的部分功能。 the None的結果仍然是'b類型，但它是某種任意（因此「未定義」）值類型'b，其中我們可以證明什麼都沒有。

來源

2015-12-18 09:41:59 chris

如何從已定義的選項中提取具體值

回答

相關問題