// Map
module ck/mapck/map

type skewnessck/map/skewness: V
  Lck/map/L: skewness
  Eck/map/E: skewness
  Rck/map/R: skewness

type treeck/map/tree: (V, V) -> V<kk: V,vv: V>
  Empck/map/Emp: forall<a,b> tree<a,b>
  Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>{ key: kk: V; value: vv: V; skew: skewnessck/map/skewness: V; left: treeck/map/tree: (V, V) -> V<kk: V,vv: V>; right: treeck/map/tree: (V, V) -> V<kk: V,vv: V> }

// Note: `map<k,v>` stores the number of key-value pairs, `size'`, in order to
// compute it in constant time, not in logarithmic time.

abstract value struct mapck/map/map: (V, V) -> V<kk: V,vv: V>
  treeck/map/map/tree: forall<a,b> (map : map<a,b>) -> tree<a,b>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>
  size'ck/map/map/size': forall<a,b> (map : map<a,b>) -> int: intstd/core/types/int: V

// Return the number of key-value pairs.
// The time complexity is O(1).
pub fun sizeck/map/size: forall<a,b> (m : map<a,b>) -> int(mm: map<$485,$486>: mapck/map/map: (V, V) -> V<kk: V,vv: V>)result: -> total int: intstd/core/types/int: V
  mm: map<$485,$486>.size'ck/map/map/size': (map : map<$485,$486>) -> int

fun skewness/showck/map/skewness/show: (s : skewness) -> string(ss: skewness: skewnessck/map/skewness: V)result: -> total string: stringstd/core/types/string: V
  match ss: skewness
    Lck/map/L: skewness -> "L"literal: string
count= 1
    Eck/map/E: skewness -> "E"literal: string
count= 1
    Rck/map/R: skewness -> "R"literal: string
count= 1

fun tree/showck/map/tree/show: forall<a,b> (t : tree<a,b>, @implicit/k/show : (a) -> string, @implicit/v/show : (b) -> string) -> string(tt: tree<$699,$700>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, @implicit/k/show?k/show: ($699) -> string: kk: V -> stringstd/core/types/string: V, @implicit/v/show?v/show: ($700) -> string: vv: V -> stringstd/core/types/string: V)result: -> total string: stringstd/core/types/string: V
  match tt: tree<$699,$700>
    Empck/map/Emp: forall<a,b> tree<a,b> -> "Emp"literal: string
count= 3
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $699, vv: $700, ss: skewness, ll: tree<$699,$700>, rr: tree<$699,$700>) ->
      "Bra("literal: string
count= 4 ++std/core/types/(++): (x : string, y : string) -> string kk: $699.show?k/show: ($699) -> string ++std/core/types/(++): (x : string, y : string) -> string ", "literal: string
count= 2 ++std/core/types/(++): (x : string, y : string) -> string vv: $700.show?v/show: ($700) -> string ++std/core/types/(++): (x : string, y : string) -> string ", "literal: string
count= 2 ++std/core/types/(++): (x : string, y : string) -> string ss: skewness.showck/map/skewness/show: (s : skewness) -> string ++std/core/types/(++): (x : string, y : string) -> string ", "literal: string
count= 2 ++std/core/types/(++): (x : string, y : string) -> string ll: tree<$699,$700>.showck/map/tree/show: (t : tree<$699,$700>, @implicit/k/show : ($699) -> string, @implicit/v/show : ($700) -> string) -> string
?k/show=?k/show
?v/show=?v/show ++std/core/types/(++): (x : string, y : string) -> string ", "literal: string
count= 2 ++std/core/types/(++): (x : string, y : string) -> string rr: tree<$699,$700>.showck/map/tree/show: (t : tree<$699,$700>, @implicit/k/show : ($699) -> string, @implicit/v/show : ($700) -> string) -> string
?k/show=?k/show
?v/show=?v/show ++std/core/types/(++): (x : string, y : string) -> string ")"literal: string
count= 1

pub fun map/showck/map/map/show: forall<a,b> (m : map<a,b>, @implicit/k/show : (a) -> string, @implicit/v/show : (b) -> string) -> string(mm: map<$528,$529>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, @implicit/k/show?k/show: ($528) -> string: kk: V -> stringstd/core/types/string: V, @implicit/v/show?v/show: ($529) -> string: vv: V -> stringstd/core/types/string: V)result: -> total string: stringstd/core/types/string: V
  mm: map<$528,$529>.treeck/map/map/tree: (map : map<$528,$529>) -> tree<$528,$529>.showck/map/tree/show: (t : tree<$528,$529>, @implicit/k/show : ($528) -> string, @implicit/v/show : ($529) -> string) -> string
?k/show=?k/show
?v/show=?v/show

// Check whether a map is empty.
pub fun is-emptyck/map/is-empty: forall<a,b> (m : map<a,b>) -> bool(mm: map<$1336,$1337>: mapck/map/map: (V, V) -> V<kk: V,vv: V>)result: -> total bool: boolstd/core/types/bool: V
  match mm: map<$1336,$1337>.treeck/map/map/tree: (map : map<$1336,$1337>) -> tree<$1336,$1337>
    Empck/map/Emp: forall<a,b> tree<a,b> -> Truestd/core/types/True: bool
    _ -> Falsestd/core/types/False: bool

// Create an empty map.
pub val emptyck/map/empty: forall<a,b> map<a,b>: forall<kk: V,vv: V> mapck/map/map: (V, V) -> V<kk: V,vv: V> = Mapck/map/Map: forall<a,b> (tree : tree<a,b>, size' : int) -> map<a,b>(Empck/map/Emp: forall<a,b> tree<a,b>, 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000)

fun tree/containsck/map/tree/contains: forall<a,b> (t : tree<a,b>, key : a, @implicit/cmp : (a, a) -> order) -> bool(tt: tree<$1536,$1537>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, keykey: $1536: kk: V, @implicit/cmp?cmp: ($1536, $1536) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total bool: boolstd/core/types/bool: V
  match tt: tree<$1536,$1537>
    Empck/map/Emp: forall<a,b> tree<a,b> -> Falsestd/core/types/False: bool
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $1536, _, _, _, _) | keykey: $1536 ==std/core/default/cmp/(==): (x : $1536, y : $1536, @implicit/cmp : ($1536, $1536) -> order) -> bool
?cmp=?cmp kk: $1536 -> Truestd/core/types/True: bool
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $1536, _, _, ll: tree<$1536,$1537>, _) | keykey: $1536 <std/core/default/cmp/(<): (x : $1536, y : $1536, @implicit/cmp : ($1536, $1536) -> order) -> bool
?cmp=?cmp kk: $1536 -> ll: tree<$1536,$1537>.containsck/map/tree/contains: (t : tree<$1536,$1537>, key : $1536, @implicit/cmp : ($1536, $1536) -> order) -> bool
?cmp=?cmp(keykey: $1536)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(_, _, _, _, rr: tree<$1536,$1537>) -> rr: tree<$1536,$1537>.containsck/map/tree/contains: (t : tree<$1536,$1537>, key : $1536, @implicit/cmp : ($1536, $1536) -> order) -> bool
?cmp=?cmp(keykey: $1536)

// Check whether a map contains a key.
// The time complexity is O(log size).
pub fun containsck/map/contains: forall<a,b> (m : map<a,b>, key : a, @implicit/cmp : (a, a) -> order) -> bool(mm: map<$1415,$1416>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, keykey: $1415: kk: V, @implicit/cmp?cmp: ($1415, $1415) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total bool: boolstd/core/types/bool: V
  mm: map<$1415,$1416>.treeck/map/map/tree: (map : map<$1415,$1416>) -> tree<$1415,$1416>.containsck/map/tree/contains: (t : tree<$1415,$1416>, key : $1415, @implicit/cmp : ($1415, $1415) -> order) -> bool
?cmp=?cmp(keykey: $1415)

// 左の部分木が 2 だけ高くなっていたら修正する
// 要素の挿入の場合、この関数を呼び出すのは左の部分木に挿入したときだが、
// 要素の削除の場合、「右」の部分木から削除したときであり、逆になるので注意が必要
// 2番目の戻り値が True のとき、修正前後で木の高さは変わらない
fun adjust-leftck/map/adjust-left: forall<a,b> (t : tree<a,b>) -> (tree<a,b>, bool)(tt: tree<$1929,$1930>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>)result: -> total (tree<2332,2333>, bool): (std/core/types/tuple2: (V, V) -> Vtreeck/map/tree: (V, V) -> V<kk: V,vv: V>, boolstd/core/types/bool: V)
  // a, b, c: keys
  // x, y, z: values
  match tt: tree<$1929,$1930>
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Eck/map/E: skewness, ll: tree<$1929,$1930>, rr: tree<$1929,$1930>) -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, ll: tree<$1929,$1930>, rr: tree<$1929,$1930>), Truestd/core/types/True: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Rck/map/R: skewness, ll: tree<$1929,$1930>, rr: tree<$1929,$1930>) -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Eck/map/E: skewness, ll: tree<$1929,$1930>, rr: tree<$1929,$1930>), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Lck/map/L: skewness, l'l': tree<$1929,$1930>, r'r': tree<$1929,$1930>), rr: tree<$1929,$1930>) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Eck/map/E: skewness, l'l': tree<$1929,$1930>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Eck/map/E: skewness, r'r': tree<$1929,$1930>, rr: tree<$1929,$1930>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Eck/map/E: skewness, l'l': tree<$1929,$1930>, r'r': tree<$1929,$1930>), rr: tree<$1929,$1930>) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Rck/map/R: skewness, l'l': tree<$1929,$1930>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, r'r': tree<$1929,$1930>, rr: tree<$1929,$1930>)), Truestd/core/types/True: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Rck/map/R: skewness, l'l': tree<$1929,$1930>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $1929, zz: $1930, Lck/map/L: skewness, l''l'': tree<$1929,$1930>, r''r'': tree<$1929,$1930>)), rr: tree<$1929,$1930>) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $1929, zz: $1930, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Eck/map/E: skewness, l'l': tree<$1929,$1930>, l''l'': tree<$1929,$1930>), Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Rck/map/R: skewness, r''r'': tree<$1929,$1930>, rr: tree<$1929,$1930>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Rck/map/R: skewness, l'l': tree<$1929,$1930>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $1929, zz: $1930, Eck/map/E: skewness, l''l'': tree<$1929,$1930>, r''r'': tree<$1929,$1930>)), rr: tree<$1929,$1930>) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $1929, zz: $1930, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Eck/map/E: skewness, l'l': tree<$1929,$1930>, l''l'': tree<$1929,$1930>), Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Eck/map/E: skewness, r''r'': tree<$1929,$1930>, rr: tree<$1929,$1930>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Rck/map/R: skewness, l'l': tree<$1929,$1930>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $1929, zz: $1930, Rck/map/R: skewness, l''l'': tree<$1929,$1930>, r''r'': tree<$1929,$1930>)), rr: tree<$1929,$1930>) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $1929, zz: $1930, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $1929, yy: $1930, Lck/map/L: skewness, l'l': tree<$1929,$1930>, l''l'': tree<$1929,$1930>), Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $1929, xx: $1930, Eck/map/E: skewness, r''r'': tree<$1929,$1930>, rr: tree<$1929,$1930>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    _ -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)tt: tree<$1929,$1930>, Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) // for exhaustive check

fun adjust-rightck/map/adjust-right: forall<a,b> (t : tree<a,b>) -> (tree<a,b>, bool)(tt: tree<$2341,$2342>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>)result: -> total (tree<2744,2745>, bool): (std/core/types/tuple2: (V, V) -> Vtreeck/map/tree: (V, V) -> V<kk: V,vv: V>, boolstd/core/types/bool: V)
  match tt: tree<$2341,$2342>
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Lck/map/L: skewness, ll: tree<$2341,$2342>, rr: tree<$2341,$2342>) -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Eck/map/E: skewness, ll: tree<$2341,$2342>, rr: tree<$2341,$2342>), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Eck/map/E: skewness, ll: tree<$2341,$2342>, rr: tree<$2341,$2342>) -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, rr: tree<$2341,$2342>), Truestd/core/types/True: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Rck/map/R: skewness, l'l': tree<$2341,$2342>, r'r': tree<$2341,$2342>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Eck/map/E: skewness, ll: tree<$2341,$2342>, l'l': tree<$2341,$2342>), r'r': tree<$2341,$2342>), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Eck/map/E: skewness, l'l': tree<$2341,$2342>, r'r': tree<$2341,$2342>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, l'l': tree<$2341,$2342>), r'r': tree<$2341,$2342>), Truestd/core/types/True: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $2341, zz: $2342, Lck/map/L: skewness, l''l'': tree<$2341,$2342>, r''r'': tree<$2341,$2342>), r'r': tree<$2341,$2342>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $2341, zz: $2342, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Eck/map/E: skewness, ll: tree<$2341,$2342>, l''l'': tree<$2341,$2342>), Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Rck/map/R: skewness, r''r'': tree<$2341,$2342>, r'r': tree<$2341,$2342>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $2341, zz: $2342, Eck/map/E: skewness, l''l'': tree<$2341,$2342>, r''r'': tree<$2341,$2342>), r'r': tree<$2341,$2342>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $2341, zz: $2342, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Eck/map/E: skewness, ll: tree<$2341,$2342>, l''l'': tree<$2341,$2342>), Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Eck/map/E: skewness, r''r'': tree<$2341,$2342>, r'r': tree<$2341,$2342>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Rck/map/R: skewness, ll: tree<$2341,$2342>, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Lck/map/L: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $2341, zz: $2342, Rck/map/R: skewness, l''l'': tree<$2341,$2342>, r''r'': tree<$2341,$2342>), r'r': tree<$2341,$2342>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(cc: $2341, zz: $2342, Eck/map/E: skewness, Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(aa: $2341, xx: $2342, Lck/map/L: skewness, ll: tree<$2341,$2342>, l''l'': tree<$2341,$2342>), Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(bb: $2341, yy: $2342, Eck/map/E: skewness, r''r'': tree<$2341,$2342>, r'r': tree<$2341,$2342>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    _ -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)tt: tree<$2341,$2342>, Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) // for exhaustive check

// add-intl(t, key, value) = (t', grown, added)
//    t' : t に (key, value) を挿入して得られる木
// grown : 高さが 1 増えたか
// added : key が追加されたか
fun add-intlck/map/add-intl: forall<a,b> (t : tree<a,b>, key : a, value : b, @implicit/cmp : (a, a) -> order) -> (tree<a,b>, bool, bool)(tt: tree<$2753,$2754>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, keykey: $2753: kk: V, valuevalue: $2754: vv: V, @implicit/cmp?cmp: ($2753, $2753) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total (tree<3318,3319>, bool, bool): (std/core/types/tuple3: (V, V, V) -> Vtreeck/map/tree: (V, V) -> V<kk: V,vv: V>, boolstd/core/types/bool: V, boolstd/core/types/bool: V)
  match tt: tree<$2753,$2754>
    Empck/map/Emp: forall<a,b> tree<a,b> -> (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(keykey: $2753, valuevalue: $2754, Eck/map/E: skewness, Empck/map/Emp: forall<a,b> tree<a,b>, Empck/map/Emp: forall<a,b> tree<a,b>), Truestd/core/types/True: bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $2753, _, ss: skewness, ll: tree<$2753,$2754>, rr: tree<$2753,$2754>) | keykey: $2753 ==std/core/default/cmp/(==): (x : $2753, y : $2753, @implicit/cmp : ($2753, $2753) -> order) -> bool
?cmp=?cmp kk: $2753 ->
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $2753, valuevalue: $2754, ss: skewness, ll: tree<$2753,$2754>, rr: tree<$2753,$2754>), Falsestd/core/types/False: bool, Falsestd/core/types/False: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) // key がすでに存在するときは値を更新する
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $2753, vv: $2754, ss: skewness, ll: tree<$2753,$2754>, rr: tree<$2753,$2754>) | keykey: $2753 <std/core/default/cmp/(<): (x : $2753, y : $2753, @implicit/cmp : ($2753, $2753) -> order) -> bool
?cmp=?cmp kk: $2753 ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': tree<$2753,$2754>, growngrown: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: tree<$2753,$2754>.add-intlck/map/add-intl: (t : tree<$2753,$2754>, key : $2753, value : $2754, @implicit/cmp : ($2753, $2753) -> order) -> (tree<$2753,$2754>, bool, bool)
?cmp=?cmp(keykey: $2753, valuevalue: $2754)
      val t't': tree<$2753,$2754> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $2753, vv: $2754, ss: skewness, l'l': tree<$2753,$2754>, rr: tree<$2753,$2754>)
      if !std/core/types/bool/(!): (b : bool) -> boolgrowngrown: bool then returnreturn: (tree<$2753,$2754>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$2753,$2754>, Falsestd/core/types/False: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': tree<$2753,$2754>, grown'grown': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$2753,$2754>.adjust-leftck/map/adjust-left: (t : tree<$2753,$2754>) -> (tree<$2753,$2754>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$2753,$2754>, grown'grown': bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $2753, vv: $2754, ss: skewness, ll: tree<$2753,$2754>, rr: tree<$2753,$2754>) ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': tree<$2753,$2754>, growngrown: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: tree<$2753,$2754>.add-intlck/map/add-intl: (t : tree<$2753,$2754>, key : $2753, value : $2754, @implicit/cmp : ($2753, $2753) -> order) -> (tree<$2753,$2754>, bool, bool)
?cmp=?cmp(keykey: $2753, valuevalue: $2754)
      val t't': tree<$2753,$2754> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $2753, vv: $2754, ss: skewness, ll: tree<$2753,$2754>, r'r': tree<$2753,$2754>)
      if !std/core/types/bool/(!): (b : bool) -> boolgrowngrown: bool then returnreturn: (tree<$2753,$2754>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$2753,$2754>, Falsestd/core/types/False: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': tree<$2753,$2754>, grown'grown': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$2753,$2754>.adjust-rightck/map/adjust-right: (t : tree<$2753,$2754>) -> (tree<$2753,$2754>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$2753,$2754>, grown'grown': bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)

// Add a key-value pair to a map.
// If the given key already exists, update the corresponding value.
// The time complexity is O(log size).
pub fun addck/map/add: forall<a,b> (m : map<a,b>, key : a, value : b, @implicit/cmp : (a, a) -> order) -> map<a,b>(mm: map<$3327,$3328>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, keykey: $3327: kk: V, valuevalue: $3328: vv: V, @implicit/cmp?cmp: ($3327, $3327) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total map<3470,3471>: mapck/map/map: (V, V) -> V<kk: V,vv: V>
  val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)tt: tree<$3327,$3328>, _, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = mm: map<$3327,$3328>.treeck/map/map/tree: (map : map<$3327,$3328>) -> tree<$3327,$3328>.add-intlck/map/add-intl: (t : tree<$3327,$3328>, key : $3327, value : $3328, @implicit/cmp : ($3327, $3327) -> order) -> (tree<$3327,$3328>, bool, bool)
?cmp=?cmp(keykey: $3327, valuevalue: $3328)
  Mapck/map/Map: forall<a,b> (tree : tree<a,b>, size' : int) -> map<a,b>(tt: tree<$3327,$3328>, if addedadded: bool then mm: map<$3327,$3328>.sizeck/map/size: (m : map<$3327,$3328>) -> int +std/core/int/(+): (x : int, y : int) -> int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001 else mm: map<$3327,$3328>.sizeck/map/size: (m : map<$3327,$3328>) -> int)

// update-intl(m, key, f) = (m', grown)
//    m' : key の頂点を更新または追加した m
// grown : 高さが 1 増えたか
// added : key が追加されたか
fun update-intlck/map/update-intl: forall<e,a,b> (t : tree<a,b>, key : a, f : (maybe<b>) -> e b, @implicit/cmp : (a, a) -> order) -> e (tree<a,b>, bool, bool)(tt: tree<$3480,$3481>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, keykey: $3480: kk: V, ff: (maybe<$3481>) -> $3479 $3481: maybestd/core/types/maybe: V -> V<vv: V> -> ee: E vv: V, @implicit/cmp?cmp: ($3480, $3480) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> 4065 (tree<4066,4067>, bool, bool): ee: E (std/core/types/tuple3: (V, V, V) -> Vtreeck/map/tree: (V, V) -> V<kk: V,vv: V>, boolstd/core/types/bool: V, boolstd/core/types/bool: V)
  match tt: tree<$3480,$3481>
    Empck/map/Emp: forall<a,b> tree<a,b> ->
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(keykey: $3480, ff: (maybe<$3481>) -> $3479 $3481(Nothingstd/core/types/Nothing: forall<a> maybe<a>), Eck/map/E: skewness, Empck/map/Emp: forall<a,b> tree<a,b>, Empck/map/Emp: forall<a,b> tree<a,b>), Truestd/core/types/True: bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) // key を追加
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $3480, vv: $3481, ss: skewness, ll: tree<$3480,$3481>, rr: tree<$3480,$3481>) | keykey: $3480 ==std/core/default/cmp/(==): (x : $3480, y : $3480, @implicit/cmp : ($3480, $3480) -> order) -> bool
?cmp=?cmp kk: $3480 ->
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $3480, ff: (maybe<$3481>) -> $3479 $3481(Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $3481)), ss: skewness, ll: tree<$3480,$3481>, rr: tree<$3480,$3481>), Falsestd/core/types/False: bool, Falsestd/core/types/False: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) // key がすでに存在するときは値を更新
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $3480, vv: $3481, ss: skewness, ll: tree<$3480,$3481>, rr: tree<$3480,$3481>) | keykey: $3480 <std/core/default/cmp/(<): (x : $3480, y : $3480, @implicit/cmp : ($3480, $3480) -> order) -> bool
?cmp=?cmp kk: $3480 ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': tree<$3480,$3481>, growngrown: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: tree<$3480,$3481>.update-intlck/map/update-intl: (t : tree<$3480,$3481>, key : $3480, f : (maybe<$3481>) -> $3479 $3481, @implicit/cmp : ($3480, $3480) -> order) -> $3479 (tree<$3480,$3481>, bool, bool)
?cmp=?cmp(keykey: $3480, ff: (maybe<$3481>) -> $3479 $3481)
      val t't': tree<$3480,$3481> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $3480, vv: $3481, ss: skewness, l'l': tree<$3480,$3481>, rr: tree<$3480,$3481>)
      if !std/core/types/bool/(!): (b : bool) -> $3479 boolgrowngrown: bool then returnreturn: (tree<$3480,$3481>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$3480,$3481>, Falsestd/core/types/False: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': tree<$3480,$3481>, grown'grown': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$3480,$3481>.adjust-leftck/map/adjust-left: (t : tree<$3480,$3481>) -> $3479 (tree<$3480,$3481>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$3480,$3481>, grown'grown': bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $3480, vv: $3481, ss: skewness, ll: tree<$3480,$3481>, rr: tree<$3480,$3481>) ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': tree<$3480,$3481>, growngrown: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: tree<$3480,$3481>.update-intlck/map/update-intl: (t : tree<$3480,$3481>, key : $3480, f : (maybe<$3481>) -> $3479 $3481, @implicit/cmp : ($3480, $3480) -> order) -> $3479 (tree<$3480,$3481>, bool, bool)
?cmp=?cmp(keykey: $3480, ff: (maybe<$3481>) -> $3479 $3481)
      val t't': tree<$3480,$3481> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $3480, vv: $3481, ss: skewness, ll: tree<$3480,$3481>, r'r': tree<$3480,$3481>)
      if !std/core/types/bool/(!): (b : bool) -> $3479 boolgrowngrown: bool then returnreturn: (tree<$3480,$3481>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$3480,$3481>, Falsestd/core/types/False: bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': tree<$3480,$3481>, grown'grown': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$3480,$3481>.adjust-rightck/map/adjust-right: (t : tree<$3480,$3481>) -> $3479 (tree<$3480,$3481>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$3480,$3481>, grown'grown': bool, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)

// Update the key-value pair of a specified key.
// If `key` already exists, replace the corresponding value `v` with `f(Just(v))`.
// Otherwise, add the pair of `key` and `f(Nothing)`.
// The time complexity is O(log size).
pub fun updateck/map/update: forall<e,a,b> (m : map<a,b>, key : a, f : (maybe<b>) -> e b, @implicit/cmp : (a, a) -> order) -> e map<a,b>(mm: map<$4078,$4079>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, keykey: $4078: kk: V, ff: (maybe<$4079>) -> $4077 $4079: maybestd/core/types/maybe: V -> V<vv: V> -> ee: E vv: V, @implicit/cmp?cmp: ($4078, $4078) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> 4226 map<4227,4228>: ee: E mapck/map/map: (V, V) -> V<kk: V,vv: V>
  val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)tt: tree<$4078,$4079>, _, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = mm: map<$4078,$4079>.treeck/map/map/tree: (map : map<$4078,$4079>) -> $4077 tree<$4078,$4079>.update-intlck/map/update-intl: (t : tree<$4078,$4079>, key : $4078, f : (maybe<$4079>) -> $4077 $4079, @implicit/cmp : ($4078, $4078) -> order) -> $4077 (tree<$4078,$4079>, bool, bool)
?cmp=?cmp(keykey: $4078, ff: (maybe<$4079>) -> $4077 $4079)
  Mapck/map/Map: forall<a,b> (tree : tree<a,b>, size' : int) -> map<a,b>(tt: tree<$4078,$4079>, if addedadded: bool then mm: map<$4078,$4079>.sizeck/map/size: (m : map<$4078,$4079>) -> $4077 int +std/core/int/(+): (x : int, y : int) -> $4077 int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001 else mm: map<$4078,$4079>.sizeck/map/size: (m : map<$4078,$4079>) -> $4077 int)

fun tree/min-bindingck/map/tree/min-binding: forall<a,b> (t : tree<a,b>) -> maybe<(a, b)>(tt: tree<$4279,$4280>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>)result: -> total maybe<(4357, 4358)>: maybestd/core/types/maybe: V -> V<(std/core/types/tuple2: (V, V) -> Vkk: V, vv: V)>
  match tt: tree<$4279,$4280>
    Empck/map/Emp: forall<a,b> tree<a,b> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $4279, vv: $4280, _, Empck/map/Emp: forall<a,b> tree<a,b>, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)kk: $4279, vv: $4280)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b))
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(_, _, _, ll: tree<$4279,$4280>, _) -> ll: tree<$4279,$4280>.min-bindingck/map/tree/min-binding: (t : tree<$4279,$4280>) -> maybe<($4279, $4280)>

// Return the key-value pair of the smallest key in a map.
// The time complexity is O(log size).
pub fun min-bindingck/map/min-binding: forall<a,b> (m : map<a,b>) -> maybe<(a, b)>(mm: map<$4238,$4239>: mapck/map/map: (V, V) -> V<kk: V,vv: V>)result: -> total maybe<(4277, 4278)>: maybestd/core/types/maybe: V -> V<(std/core/types/tuple2: (V, V) -> Vkk: V, vv: V)>
  mm: map<$4238,$4239>.treeck/map/map/tree: (map : map<$4238,$4239>) -> tree<$4238,$4239>.min-bindingck/map/tree/min-binding: (t : tree<$4238,$4239>) -> maybe<($4238, $4239)>

fun tree/max-bindingck/map/tree/max-binding: forall<a,b> (t : tree<a,b>) -> maybe<(a, b)>(tt: tree<$4419,$4420>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>)result: -> total maybe<(4497, 4498)>: maybestd/core/types/maybe: V -> V<(std/core/types/tuple2: (V, V) -> Vkk: V, vv: V)>
  match tt: tree<$4419,$4420>
    Empck/map/Emp: forall<a,b> tree<a,b> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $4419, vv: $4420, _, _, Empck/map/Emp: forall<a,b> tree<a,b>) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)kk: $4419, vv: $4420)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b))
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(_, _, _, _, rr: tree<$4419,$4420>) -> rr: tree<$4419,$4420>.max-bindingck/map/tree/max-binding: (t : tree<$4419,$4420>) -> maybe<($4419, $4420)>

// Return the key-value pair of the largest key in a map.
// The time complexity is O(log size).
pub fun max-bindingck/map/max-binding: forall<a,b> (m : map<a,b>) -> maybe<(a, b)>(mm: map<$4378,$4379>: mapck/map/map: (V, V) -> V<kk: V,vv: V>)result: -> total maybe<(4417, 4418)>: maybestd/core/types/maybe: V -> V<(std/core/types/tuple2: (V, V) -> Vkk: V, vv: V)>
  mm: map<$4378,$4379>.treeck/map/map/tree: (map : map<$4378,$4379>) -> tree<$4378,$4379>.max-bindingck/map/tree/max-binding: (t : tree<$4378,$4379>) -> maybe<($4378, $4379)>

// remove-intl(t, key) = (t', shrinked, deleted)
//          t' : t から key をなくした木
//    shrinked : 高さが 1 減ったか
//     deleted : key を削除したか (元からなければ False)
fun remove-intlck/map/remove-intl: forall<a,b> (t : tree<a,b>, key : a, @implicit/cmp : (a, a) -> order) -> (tree<a,b>, bool, bool)(tt: tree<$4518,$4519>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, keykey: $4518: kk: V, @implicit/cmp?cmp: ($4518, $4518) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total (tree<5417,5418>, bool, bool): (std/core/types/tuple3: (V, V, V) -> Vtreeck/map/tree: (V, V) -> V<kk: V,vv: V>, boolstd/core/types/bool: V, boolstd/core/types/bool: V)
  match tt: tree<$4518,$4519>
    Empck/map/Emp: forall<a,b> tree<a,b> -> (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/map/Emp: forall<a,b> tree<a,b>, Falsestd/core/types/False: bool, Falsestd/core/types/False: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $4518, vv: $4519, ss: skewness, ll: tree<$4518,$4519>, rr: tree<$4518,$4519>) | keykey: $4518 <std/core/default/cmp/(<): (x : $4518, y : $4518, @implicit/cmp : ($4518, $4518) -> order) -> bool
?cmp=?cmp kk: $4518 ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': tree<$4518,$4519>, shrinkedshrinked: bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: tree<$4518,$4519>.remove-intlck/map/remove-intl: (t : tree<$4518,$4519>, key : $4518, @implicit/cmp : ($4518, $4518) -> order) -> (tree<$4518,$4519>, bool, bool)
?cmp=?cmp(keykey: $4518)
      val m'm': tree<$4518,$4519> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $4518, vv: $4519, ss: skewness, l'l': tree<$4518,$4519>, rr: tree<$4518,$4519>)
      if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$4518,$4519>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m'm': tree<$4518,$4519>, Falsestd/core/types/False: bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)m''m'': tree<$4518,$4519>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = m'm': tree<$4518,$4519>.adjust-rightck/map/adjust-right: (t : tree<$4518,$4519>) -> (tree<$4518,$4519>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m''m'': tree<$4518,$4519>, !std/core/types/bool/(!): (b : bool) -> boolnot-shrinked'not-shrinked': bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $4518, vv: $4519, ss: skewness, ll: tree<$4518,$4519>, rr: tree<$4518,$4519>) | keykey: $4518 >std/core/default/cmp/(>): (x : $4518, y : $4518, @implicit/cmp : ($4518, $4518) -> order) -> bool
?cmp=?cmp kk: $4518 ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': tree<$4518,$4519>, shrinkedshrinked: bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: tree<$4518,$4519>.remove-intlck/map/remove-intl: (t : tree<$4518,$4519>, key : $4518, @implicit/cmp : ($4518, $4518) -> order) -> (tree<$4518,$4519>, bool, bool)
?cmp=?cmp(keykey: $4518)
      val m'm': tree<$4518,$4519> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $4518, vv: $4519, ss: skewness, ll: tree<$4518,$4519>, r'r': tree<$4518,$4519>)
      if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$4518,$4519>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m'm': tree<$4518,$4519>, Falsestd/core/types/False: bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)m''m'': tree<$4518,$4519>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = m'm': tree<$4518,$4519>.adjust-leftck/map/adjust-left: (t : tree<$4518,$4519>) -> (tree<$4518,$4519>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m''m'': tree<$4518,$4519>, !std/core/types/bool/(!): (b : bool) -> boolnot-shrinked'not-shrinked': bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(_, _, ss: skewness, ll: tree<$4518,$4519>, rr: tree<$4518,$4519>) ->
      match rr: tree<$4518,$4519>.min-bindingck/map/tree/min-binding: (t : tree<$4518,$4519>) -> maybe<($4518, $4519)>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)min-kmin-k: $4518, min-vmin-v: $4519)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)) ->
          val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': tree<$4518,$4519>, shrinkedshrinked: bool, _)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: tree<$4518,$4519>.remove-intlck/map/remove-intl: (t : tree<$4518,$4519>, key : $4518, @implicit/cmp : ($4518, $4518) -> order) -> (tree<$4518,$4519>, bool, bool)
?cmp=?cmp(min-kmin-k: $4518)
          val m'm': tree<$4518,$4519> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(min-kmin-k: $4518, min-vmin-v: $4519, ss: skewness, ll: tree<$4518,$4519>, r'r': tree<$4518,$4519>)
          if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$4518,$4519>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m'm': tree<$4518,$4519>, Falsestd/core/types/False: bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
          val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)m''m'': tree<$4518,$4519>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = m'm': tree<$4518,$4519>.adjust-leftck/map/adjust-left: (t : tree<$4518,$4519>) -> (tree<$4518,$4519>, bool)
          returnreturn: (tree<$4518,$4519>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m''m'': tree<$4518,$4519>, !std/core/types/bool/(!): (b : bool) -> boolnot-shrinked'not-shrinked': bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
        _ -> (std/core/types/Unit: ())std/core/types/Unit: ()
      match ll: tree<$4518,$4519>.max-bindingck/map/tree/max-binding: (t : tree<$4518,$4519>) -> maybe<($4518, $4519)>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)max-kmax-k: $4518, max-vmax-v: $4519)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)) ->
          val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': tree<$4518,$4519>, shrinkedshrinked: bool, _)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: tree<$4518,$4519>.remove-intlck/map/remove-intl: (t : tree<$4518,$4519>, key : $4518, @implicit/cmp : ($4518, $4518) -> order) -> (tree<$4518,$4519>, bool, bool)
?cmp=?cmp(max-kmax-k: $4518)
          val m'm': tree<$4518,$4519> = Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(max-kmax-k: $4518, max-vmax-v: $4519, ss: skewness, l'l': tree<$4518,$4519>, rr: tree<$4518,$4519>)
          if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$4518,$4519>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m'm': tree<$4518,$4519>, Falsestd/core/types/False: bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
          val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)m''m'': tree<$4518,$4519>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = m'm': tree<$4518,$4519>.adjust-rightck/map/adjust-right: (t : tree<$4518,$4519>) -> (tree<$4518,$4519>, bool)
          returnreturn: (tree<$4518,$4519>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)m''m'': tree<$4518,$4519>, !std/core/types/bool/(!): (b : bool) -> boolnot-shrinked'not-shrinked': bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
        _ -> (std/core/types/Unit: ())std/core/types/Unit: ()
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/map/Emp: forall<a,b> tree<a,b>, Truestd/core/types/True: bool, Truestd/core/types/True: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)

// Remove a key and the corresponding value from a map.
// Do nothing if the given key does not exist.
// The time complexity is O(log size).
pub fun removeck/map/remove: forall<a,b> (m : map<a,b>, key : a, @implicit/cmp : (a, a) -> order) -> map<a,b>(mm: map<$5426,$5427>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, keykey: $5426: kk: V, @implicit/cmp?cmp: ($5426, $5426) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total map<5567,5568>: mapck/map/map: (V, V) -> V<kk: V,vv: V>
  val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)tt: tree<$5426,$5427>, _, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = mm: map<$5426,$5427>.treeck/map/map/tree: (map : map<$5426,$5427>) -> tree<$5426,$5427>.remove-intlck/map/remove-intl: (t : tree<$5426,$5427>, key : $5426, @implicit/cmp : ($5426, $5426) -> order) -> (tree<$5426,$5427>, bool, bool)
?cmp=?cmp(keykey: $5426)
  Mapck/map/Map: forall<a,b> (tree : tree<a,b>, size' : int) -> map<a,b>(tt: tree<$5426,$5427>, if deleteddeleted: bool then mm: map<$5426,$5427>.sizeck/map/size: (m : map<$5426,$5427>) -> int -std/core/int/(-): (x : int, y : int) -> int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001 else mm: map<$5426,$5427>.sizeck/map/size: (m : map<$5426,$5427>) -> int)

fun tree/getck/map/tree/get: forall<a,b> (t : tree<a,b>, key : a, @implicit/cmp : (a, a) -> order) -> maybe<b>(tt: tree<$5697,$5698>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, keykey: $5697: kk: V, @implicit/cmp?cmp: ($5697, $5697) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total maybe<6076>: maybestd/core/types/maybe: V -> V<vv: V>
  match tt: tree<$5697,$5698>
    Empck/map/Emp: forall<a,b> tree<a,b> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $5697, vv: $5698, _, _, _) | keykey: $5697 ==std/core/default/cmp/(==): (x : $5697, y : $5697, @implicit/cmp : ($5697, $5697) -> order) -> bool
?cmp=?cmp kk: $5697 -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $5698)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $5697, _, _, ll: tree<$5697,$5698>, _) | keykey: $5697 <std/core/default/cmp/(<): (x : $5697, y : $5697, @implicit/cmp : ($5697, $5697) -> order) -> bool
?cmp=?cmp kk: $5697 -> ll: tree<$5697,$5698>.getck/map/tree/get: (t : tree<$5697,$5698>, key : $5697, @implicit/cmp : ($5697, $5697) -> order) -> maybe<$5698>
?cmp=?cmp(keykey: $5697)
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(_, _, _, _, rr: tree<$5697,$5698>) -> rr: tree<$5697,$5698>.getck/map/tree/get: (t : tree<$5697,$5698>, key : $5697, @implicit/cmp : ($5697, $5697) -> order) -> maybe<$5698>
?cmp=?cmp(keykey: $5697)

// Get the value of a specified key.
// The time complexity is O(log size).
pub fun getck/map/get: forall<a,b> (m : map<a,b>, key : a, @implicit/cmp : (a, a) -> order) -> maybe<b>(mm: map<$5576,$5577>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, keykey: $5576: kk: V, @implicit/cmp?cmp: ($5576, $5576) -> order: (kk: V, kk: V) -> orderstd/core/types/order: V)result: -> total maybe<5696>: maybestd/core/types/maybe: V -> V<vv: V>
  mm: map<$5576,$5577>.treeck/map/map/tree: (map : map<$5576,$5577>) -> tree<$5576,$5577>.getck/map/tree/get: (t : tree<$5576,$5577>, key : $5576, @implicit/cmp : ($5576, $5576) -> order) -> maybe<$5577>
?cmp=?cmp(keykey: $5576)

fun tree/foreachck/map/tree/foreach: forall<e,a,b> (t : tree<a,b>, action : (a, b) -> e ()) -> e ()(tt: tree<$6161,$6162>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, actionaction: ($6161, $6162) -> $6160 (): (kk: V, vv: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V)result: -> 6266 (): ee: E(std/core/types/unit: V)std/core/types/unit: V
  match tt: tree<$6161,$6162>
    Empck/map/Emp: forall<a,b> tree<a,b> -> (std/core/types/Unit: ())std/core/types/Unit: ()
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $6161, vv: $6162, _, ll: tree<$6161,$6162>, rr: tree<$6161,$6162>) ->
      ll: tree<$6161,$6162>.foreachck/map/tree/foreach: (t : tree<$6161,$6162>, action : ($6161, $6162) -> $6160 ()) -> $6160 ()(actionaction: ($6161, $6162) -> $6160 ())
      actionaction: ($6161, $6162) -> $6160 ()(kk: $6161, vv: $6162)
      rr: tree<$6161,$6162>.foreachck/map/tree/foreach: (t : tree<$6161,$6162>, action : ($6161, $6162) -> $6160 ()) -> $6160 ()(actionaction: ($6161, $6162) -> $6160 ())

// Iterate over key-value pairs in ascending order of their keys
pub fun foreachck/map/foreach: forall<e,a,b> (m : map<a,b>, action : (a, b) -> e ()) -> e ()(mm: map<$6097,$6098>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, actionaction: ($6097, $6098) -> $6096 (): (kk: V, vv: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V)result: -> 6157 (): ee: E(std/core/types/unit: V)std/core/types/unit: V
  mm: map<$6097,$6098>.treeck/map/map/tree: (map : map<$6097,$6098>) -> $6096 tree<$6097,$6098>.foreachck/map/tree/foreach: (t : tree<$6097,$6098>, action : ($6097, $6098) -> $6096 ()) -> $6096 ()(actionaction: ($6097, $6098) -> $6096 ())

fun tree/foreach-keyck/map/tree/foreach-key: forall<e,a,b> (t : tree<a,b>, action : (a) -> e ()) -> e ()(tt: tree<$6364,$6365>: treeck/map/tree: (V, V) -> V<kk: V,vv: V>, actionaction: ($6364) -> $6363 (): kk: V -> ee: E (std/core/types/unit: V)std/core/types/unit: V)result: -> 6444 (): ee: E(std/core/types/unit: V)std/core/types/unit: V
  match tt: tree<$6364,$6365>
    Empck/map/Emp: forall<a,b> tree<a,b> -> (std/core/types/Unit: ())std/core/types/Unit: ()
    Brack/map/Bra: forall<a,b> (key : a, value : b, skew : skewness, left : tree<a,b>, right : tree<a,b>) -> tree<a,b>(kk: $6364, _, _, ll: tree<$6364,$6365>, rr: tree<$6364,$6365>) ->
      ll: tree<$6364,$6365>.foreach-keyck/map/tree/foreach-key: (t : tree<$6364,$6365>, action : ($6364) -> $6363 ()) -> $6363 ()(actionaction: ($6364) -> $6363 ())
      actionaction: ($6364) -> $6363 ()(kk: $6364)
      rr: tree<$6364,$6365>.foreach-keyck/map/tree/foreach-key: (t : tree<$6364,$6365>, action : ($6364) -> $6363 ()) -> $6363 ()(actionaction: ($6364) -> $6363 ())

// Iterate over keys in ascending order
pub fun foreach-keyck/map/foreach-key: forall<e,a,b> (m : map<a,b>, action : (a) -> e ()) -> e ()(mm: map<$6312,$6313>: mapck/map/map: (V, V) -> V<kk: V,vv: V>, actionaction: ($6312) -> $6311 (): kk: V -> ee: E (std/core/types/unit: V)std/core/types/unit: V)result: -> 6360 (): ee: E(std/core/types/unit: V)std/core/types/unit: V
  mm: map<$6312,$6313>.treeck/map/map/tree: (map : map<$6312,$6313>) -> $6311 tree<$6312,$6313>.foreach-keyck/map/tree/foreach-key: (t : tree<$6312,$6313>, action : ($6312) -> $6311 ()) -> $6311 ()(actionaction: ($6312) -> $6311 ())