HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-07-14 22:50:28 +03:00
Code Issues Packages Projects Releases Wiki Activity

Add commented version of BBT maps to String and U60

Browse Source
This commit is contained in:
Derenash 2024-02-21 12:11:42 -03:00
parent 0e97867813
commit 627cc96777
2 changed files with 77 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
book/String.Map.kind2
View File

@ -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)

39
book/U60.Map.kind2
View File

@ -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)