有限域映射

我需要一個數據類型的有限映射。我使用典型的（部分）地圖，直到我在證明中碰到一個路障，只能通過引入一個finite (dom m)謂詞來修復。將這個事實進行到底是乏味的，那麼標準庫中是否有一些解決方案呢？有限域映射

2017-04-26 Sebastian Graf

正如在this answer（我也從中偷走了下面的例子）中提到的那樣，中有一個有限映射類型fmap，因爲Isabelle2016-1。

theory Scratch 
    imports "~~/src/HOL/Library/Finite_Map" 
begin 

value "fmdom' (fmap_of_list [(1, 2), (3, 4::nat)])" 
(* prints "{1, 1 + 1 + 1}" *)

來源

2017-04-26 21:00:22

我字面上搜索了5次，然後觸及引用的答案。最好的結果來自2006年的郵件列表線程，所以我想讓這更適合搜索引擎優化。 –

回答

相關問題