diff --git a/book/String.Map.kind2 b/book/String.Map.kind2 index b465499e..577087a9 100644 --- a/book/String.Map.kind2 +++ b/book/String.Map.kind2 @@ -25,3 +25,41 @@ String.Map.new : ∀(V: *) (String.Map V) = λV (List.Map.new String V) + +// BBT Version + +// String.Map +// : ∀(V: *) +// * +// = λV (BBT String V) + +// String.Map.get +// : ∀(V: *) +// ∀(key: String) +// ∀(map: (String.Map V)) +// (Maybe V) +// = λV λkey λmap +// (BBT.get String V String.cmp key map) + +// String.Map.got +// : ∀(V: *) +// ∀(key: String) +// ∀(map: (String.Map V)) +// (Pair (Maybe V) (String.Map V)) +// = λV λkey λmap +// (BBT.got String V String.cmp key map) + +// String.Map.set +// : ∀(V: *) +// ∀(key: String) +// ∀(val: V) +// ∀(map: (String.Map V)) +// (String.Map V) +// = λV λkey λval λmap +// (BBT.set String V String.cmp key val map) + +// String.Map.new +// : ∀(V: *) +// (String.Map V) +// = λV (BBT.tip String V) + diff --git a/book/U60.Map.kind2 b/book/U60.Map.kind2 index ee14a2a3..5503d47f 100644 --- a/book/U60.Map.kind2 +++ b/book/U60.Map.kind2 @@ -1,3 +1,4 @@ + // Temporarily just a list of key/val U60.Map @@ -25,3 +26,41 @@ U60.Map.new : ∀(V: *) (U60.Map V) = λV (List.Map.new #U60 V) + + +// BBT Version + +// U60.Map +// : ∀(V: *) +// * +// = λV (BBT #U60 V) + +// U60.Map.get +// : ∀(V: *) +// ∀(key: #U60) +// ∀(map: (U60.Map V)) +// (Maybe V) +// = λV λkey λmap +// (BBT.get #U60 V U60.cmp key map) + +// U60.Map.got +// : ∀(V: *) +// ∀(key: #U60) +// ∀(map: (U60.Map V)) +// (Pair (Maybe V) (U60.Map V)) +// = λV λkey λmap +// (BBT.got #U60 V U60.cmp key map) + +// U60.Map.set +// : ∀(V: *) +// ∀(key: #U60) +// ∀(val: V) +// ∀(map: (U60.Map V)) +// (U60.Map V) +// = λV λkey λval λmap +// (BBT.set #U60 V U60.cmp key val map) + +// U60.Map.new +// : ∀(V: *) +// (U60.Map V) +// = λV (BBT.tip #U60 V)