// Set
module ck/setck/set

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

type treeck/set/tree: V -> V<aa: V>
  Empck/set/Emp: forall<a> tree<a>
  Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>{ value: aa: V; skew: skewnessck/set/skewness: V; left: treeck/set/tree: V -> V<aa: V>; right: treeck/set/tree: V -> V<aa: V> }

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

abstract value struct setck/set/set: V -> V<aa: V>
  treeck/set/set/tree: forall<a> (set : set<a>) -> tree<a>: treeck/set/tree: V -> V<aa: V>
  size'ck/set/set/size': forall<a> (set : set<a>) -> int: intstd/core/types/int: V

// Return the number of key-value pairs.
// The time complexity is O(1).
pub fun sizeck/set/size: forall<a> (s : set<a>) -> int(ss: set<$287>: setck/set/set: V -> V<aa: V>)result: -> total int: intstd/core/types/int: V
  ss: set<$287>.size'ck/set/set/size': (set : set<$287>) -> int

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

fun tree/showck/set/tree/show: forall<a> (t : tree<a>, @implicit/show : (a) -> string) -> string(tt: tree<$436>: treeck/set/tree: V -> V<aa: V>, @implicit/show?show: ($436) -> string: aa: V -> stringstd/core/types/string: V)result: -> total string: stringstd/core/types/string: V
  match tt: tree<$436>
    Empck/set/Emp: forall<a> tree<a> -> "Emp"literal: string
count= 3
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $436, ss: skewness, ll: tree<$436>, rr: tree<$436>) ->
      "Bra("literal: string
count= 4 ++std/core/types/(++): (x : string, y : string) -> string vv: $436.show?show: ($436) -> string ++std/core/types/(++): (x : string, y : string) -> string ", "literal: string
count= 2 ++std/core/types/(++): (x : string, y : string) -> string ss: skewness.showck/set/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<$436>.showck/set/tree/show: (t : tree<$436>, @implicit/show : ($436) -> string) -> string
?show=?show ++std/core/types/(++): (x : string, y : string) -> string ", "literal: string
count= 2 ++std/core/types/(++): (x : string, y : string) -> string rr: tree<$436>.showck/set/tree/show: (t : tree<$436>, @implicit/show : ($436) -> string) -> string
?show=?show ++std/core/types/(++): (x : string, y : string) -> string ")"literal: string
count= 1

pub fun set/showck/set/set/show: forall<a> (s : set<a>, @implicit/show : (a) -> string) -> string(ss: set<$318>: setck/set/set: V -> V<aa: V>, @implicit/show?show: ($318) -> string: aa: V -> stringstd/core/types/string: V)result: -> total string: stringstd/core/types/string: V
  ss: set<$318>.treeck/set/set/tree: (set : set<$318>) -> tree<$318>.showck/set/tree/show: (t : tree<$318>, @implicit/show : ($318) -> string) -> string
?show=?show

// Check whether a set is empty
pub fun is-emptyck/set/is-empty: forall<a> (s : set<a>) -> bool(ss: set<$872>: setck/set/set: V -> V<aa: V>)result: -> total bool: boolstd/core/types/bool: V
  match ss: set<$872>.treeck/set/set/tree: (set : set<$872>) -> tree<$872>
    Empck/set/Emp: forall<a> tree<a> -> Truestd/core/types/True: bool
    _ -> Falsestd/core/types/False: bool

// Create an empty set
pub val emptyck/set/empty: forall<a> set<a>: forall<aa: V> setck/set/set: V -> V<aa: V> = Setck/set/Set: forall<a> (tree : tree<a>, size' : int) -> set<a>(Empck/set/Emp: forall<a> tree<a>, 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000)

// Create a set with a single element
pub fun singletonck/set/singleton: forall<a> (v : a) -> set<a>(vv: $921: aa: V)result: -> total set<951>: setck/set/set: V -> V<aa: V>
  Setck/set/Set: forall<a> (tree : tree<a>, size' : int) -> set<a>(Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>( value = vv: $921, skew = Eck/set/E: skewness, left = Empck/set/Emp: forall<a> tree<a>, right = Empck/set/Emp: forall<a> tree<a> ), 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001)

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

// Check whether a value belongs to a set.
// The time complexity is O(log size).
pub fun containsck/set/contains: forall<a> (s : set<a>, value : a, @implicit/cmp : (a, a) -> order) -> bool(ss: set<$956>: setck/set/set: V -> V<aa: V>, valuevalue: $956: aa: V, @implicit/cmp?cmp: ($956, $956) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V)result: -> total bool: boolstd/core/types/bool: V
  ss: set<$956>.treeck/set/set/tree: (set : set<$956>) -> tree<$956>.containsck/set/tree/contains: (t : tree<$956>, value : $956, @implicit/cmp : ($956, $956) -> order) -> bool
?cmp=?cmp(valuevalue: $956)

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

fun adjust-rightck/set/adjust-right: forall<a> (t : tree<a>) -> (tree<a>, bool)(tt: tree<$1732>: treeck/set/tree: V -> V<aa: V>)result: -> total (tree<2040>, bool): (std/core/types/tuple2: (V, V) -> Vtreeck/set/tree: V -> V<aa: V>, boolstd/core/types/bool: V)
  match tt: tree<$1732>
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Lck/set/L: skewness, ll: tree<$1732>, rr: tree<$1732>) -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Eck/set/E: skewness, ll: tree<$1732>, rr: tree<$1732>), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Eck/set/E: skewness, ll: tree<$1732>, rr: tree<$1732>) -> (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, rr: tree<$1732>), Truestd/core/types/True: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Rck/set/R: skewness, l'l': tree<$1732>, r'r': tree<$1732>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Eck/set/E: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Eck/set/E: skewness, ll: tree<$1732>, l'l': tree<$1732>), r'r': tree<$1732>), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Eck/set/E: skewness, l'l': tree<$1732>, r'r': tree<$1732>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Lck/set/L: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, l'l': tree<$1732>), r'r': tree<$1732>), Truestd/core/types/True: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Lck/set/L: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(cc: $1732, Lck/set/L: skewness, l''l'': tree<$1732>, r''r'': tree<$1732>), r'r': tree<$1732>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(cc: $1732, Eck/set/E: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Eck/set/E: skewness, ll: tree<$1732>, l''l'': tree<$1732>), Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Rck/set/R: skewness, r''r'': tree<$1732>, r'r': tree<$1732>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Lck/set/L: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(cc: $1732, Eck/set/E: skewness, l''l'': tree<$1732>, r''r'': tree<$1732>), r'r': tree<$1732>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(cc: $1732, Eck/set/E: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Eck/set/E: skewness, ll: tree<$1732>, l''l'': tree<$1732>), Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Eck/set/E: skewness, r''r'': tree<$1732>, r'r': tree<$1732>)), Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Rck/set/R: skewness, ll: tree<$1732>, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Lck/set/L: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(cc: $1732, Rck/set/R: skewness, l''l'': tree<$1732>, r''r'': tree<$1732>), r'r': tree<$1732>)) ->
      (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(cc: $1732, Eck/set/E: skewness, Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(aa: $1732, Lck/set/L: skewness, ll: tree<$1732>, l''l'': tree<$1732>), Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(bb: $1732, Eck/set/E: skewness, r''r'': tree<$1732>, r'r': tree<$1732>)), 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<$1732>, Falsestd/core/types/False: bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) // for exhaustive check

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

// Add a value to a set.
// Do nothing if the given value already exists.
// The time complexity is O(log size).
pub fun addck/set/add: forall<a> (s : set<a>, value : a, @implicit/cmp : (a, a) -> order) -> set<a>(ss: set<$2553>: setck/set/set: V -> V<aa: V>, valuevalue: $2553: aa: V, @implicit/cmp?cmp: ($2553, $2553) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V)result: -> total set<2673>: setck/set/set: V -> V<aa: V>
  val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)tt: tree<$2553>, _, addedadded: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ss: set<$2553>.treeck/set/set/tree: (set : set<$2553>) -> tree<$2553>.add-intlck/set/add-intl: (t : tree<$2553>, value : $2553, @implicit/cmp : ($2553, $2553) -> order) -> (tree<$2553>, bool, bool)
?cmp=?cmp(valuevalue: $2553)
  Setck/set/Set: forall<a> (tree : tree<a>, size' : int) -> set<a>(tt: tree<$2553>, if addedadded: bool then ss: set<$2553>.sizeck/set/size: (s : set<$2553>) -> int +std/core/int/(+): (x : int, y : int) -> int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001 else ss: set<$2553>.sizeck/set/size: (s : set<$2553>) -> int)

fun tree/minck/set/tree/min: forall<a> (t : tree<a>) -> maybe<a>(tt: tree<$2704>: treeck/set/tree: V -> V<aa: V>)result: -> total maybe<2750>: maybestd/core/types/maybe: V -> V<aa: V>
  match tt: tree<$2704>
    Empck/set/Emp: forall<a> tree<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $2704, _, Empck/set/Emp: forall<a> tree<a>, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $2704)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(_, _, ll: tree<$2704>, _) -> ll: tree<$2704>.minck/set/tree/min: (t : tree<$2704>) -> maybe<$2704>

// Return the minimum element of a set.
// The time complexity is O(log size).
pub fun minck/set/min: forall<a> (s : set<a>) -> maybe<a>(ss: set<$2678>: setck/set/set: V -> V<aa: V>)result: -> total maybe<2703>: maybestd/core/types/maybe: V -> V<aa: V>
  ss: set<$2678>.treeck/set/set/tree: (set : set<$2678>) -> tree<$2678>.minck/set/tree/min: (t : tree<$2678>) -> maybe<$2678>

fun tree/maxck/set/tree/max: forall<a> (t : tree<a>) -> maybe<a>(tt: tree<$2790>: treeck/set/tree: V -> V<aa: V>)result: -> total maybe<2836>: maybestd/core/types/maybe: V -> V<aa: V>
  match tt: tree<$2790>
    Empck/set/Emp: forall<a> tree<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $2790, _, _, Empck/set/Emp: forall<a> tree<a>) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $2790)
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(_, _, _, rr: tree<$2790>) -> rr: tree<$2790>.maxck/set/tree/max: (t : tree<$2790>) -> maybe<$2790>

// Return the maximum element of a set.
// The time complexity is O(log size).
pub fun maxck/set/max: forall<a> (s : set<a>) -> maybe<a>(ss: set<$2764>: setck/set/set: V -> V<aa: V>)result: -> total maybe<2789>: maybestd/core/types/maybe: V -> V<aa: V>
  ss: set<$2764>.treeck/set/set/tree: (set : set<$2764>) -> tree<$2764>.maxck/set/tree/max: (t : tree<$2764>) -> maybe<$2764>

// remove-intl(t, v) = (t', shrinked, deleted)
//          t' : t から v をなくした木
//    shrinked : 高さが 1 減ったか
//     deleted : v を削除したか (元からなければ false)
fun remove-intlck/set/remove-intl: forall<a> (t : tree<a>, value : a, @implicit/cmp : (a, a) -> order) -> (tree<a>, bool, bool)(tt: tree<$2850>: treeck/set/tree: V -> V<aa: V>, valuevalue: $2850: aa: V, @implicit/cmp?cmp: ($2850, $2850) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V)result: -> total (tree<3665>, bool, bool): (std/core/types/tuple3: (V, V, V) -> Vtreeck/set/tree: V -> V<aa: V>, boolstd/core/types/bool: V, boolstd/core/types/bool: V)
  match tt: tree<$2850>
    Empck/set/Emp: forall<a> tree<a> -> (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/set/Emp: forall<a> tree<a>, 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/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $2850, ss: skewness, ll: tree<$2850>, rr: tree<$2850>) | valuevalue: $2850 <std/core/default/cmp/(<): (x : $2850, y : $2850, @implicit/cmp : ($2850, $2850) -> order) -> bool
?cmp=?cmp vv: $2850 ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': tree<$2850>, shrinkedshrinked: bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: tree<$2850>.remove-intlck/set/remove-intl: (t : tree<$2850>, value : $2850, @implicit/cmp : ($2850, $2850) -> order) -> (tree<$2850>, bool, bool)
?cmp=?cmp(valuevalue: $2850)
      val t't': tree<$2850> = Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $2850, ss: skewness, l'l': tree<$2850>, rr: tree<$2850>)
      if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$2850>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$2850>, 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)t''t'': tree<$2850>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$2850>.adjust-rightck/set/adjust-right: (t : tree<$2850>) -> (tree<$2850>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$2850>, !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/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $2850, ss: skewness, ll: tree<$2850>, rr: tree<$2850>) | valuevalue: $2850 >std/core/default/cmp/(>): (x : $2850, y : $2850, @implicit/cmp : ($2850, $2850) -> order) -> bool
?cmp=?cmp vv: $2850 ->
      val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': tree<$2850>, shrinkedshrinked: bool, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: tree<$2850>.remove-intlck/set/remove-intl: (t : tree<$2850>, value : $2850, @implicit/cmp : ($2850, $2850) -> order) -> (tree<$2850>, bool, bool)
?cmp=?cmp(valuevalue: $2850)
      val t't': tree<$2850> = Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $2850, ss: skewness, ll: tree<$2850>, r'r': tree<$2850>)
      if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$2850>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$2850>, 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)t''t'': tree<$2850>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$2850>.adjust-leftck/set/adjust-left: (t : tree<$2850>) -> (tree<$2850>, bool)
      (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$2850>, !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/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(_, ss: skewness, ll: tree<$2850>, rr: tree<$2850>) ->
      match rr: tree<$2850>.minck/set/tree/min: (t : tree<$2850>) -> maybe<$2850>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(min-vmin-v: $2850) ->
          val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': tree<$2850>, shrinkedshrinked: bool, _)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: tree<$2850>.remove-intlck/set/remove-intl: (t : tree<$2850>, value : $2850, @implicit/cmp : ($2850, $2850) -> order) -> (tree<$2850>, bool, bool)
?cmp=?cmp(min-vmin-v: $2850)
          val t't': tree<$2850> = Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(min-vmin-v: $2850, ss: skewness, ll: tree<$2850>, r'r': tree<$2850>)
          if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$2850>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$2850>, 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)t''t'': tree<$2850>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$2850>.adjust-leftck/set/adjust-left: (t : tree<$2850>) -> (tree<$2850>, bool)
          returnreturn: (tree<$2850>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$2850>, !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<$2850>.maxck/set/tree/max: (t : tree<$2850>) -> maybe<$2850>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(max-vmax-v: $2850) ->
          val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': tree<$2850>, shrinkedshrinked: bool, _)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: tree<$2850>.remove-intlck/set/remove-intl: (t : tree<$2850>, value : $2850, @implicit/cmp : ($2850, $2850) -> order) -> (tree<$2850>, bool, bool)
?cmp=?cmp(max-vmax-v: $2850)
          val t't': tree<$2850> = Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(max-vmax-v: $2850, ss: skewness, l'l': tree<$2850>, rr: tree<$2850>)
          if !std/core/types/bool/(!): (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (tree<$2850>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': tree<$2850>, 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)t''t'': tree<$2850>, not-shrinked'not-shrinked': bool)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = t't': tree<$2850>.adjust-rightck/set/adjust-right: (t : tree<$2850>) -> (tree<$2850>, bool)
          returnreturn: (tree<$2850>, bool, bool) (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': tree<$2850>, !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/set/Emp: forall<a> tree<a>, 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 an element from a set.
// Do nothing if the given value does not exist.
// The time complexity is O(log size).
pub fun removeck/set/remove: forall<a> (s : set<a>, value : a, @implicit/cmp : (a, a) -> order) -> set<a>(ss: set<$3670>: setck/set/set: V -> V<aa: V>, valuevalue: $3670: aa: V, @implicit/cmp?cmp: ($3670, $3670) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V)result: -> total set<3790>: setck/set/set: V -> V<aa: V>
  val (std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)tt: tree<$3670>, _, deleteddeleted: bool)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ss: set<$3670>.treeck/set/set/tree: (set : set<$3670>) -> tree<$3670>.remove-intlck/set/remove-intl: (t : tree<$3670>, value : $3670, @implicit/cmp : ($3670, $3670) -> order) -> (tree<$3670>, bool, bool)
?cmp=?cmp(valuevalue: $3670)
  Setck/set/Set: forall<a> (tree : tree<a>, size' : int) -> set<a>(tt: tree<$3670>, if deleteddeleted: bool then ss: set<$3670>.sizeck/set/size: (s : set<$3670>) -> int -std/core/int/(-): (x : int, y : int) -> int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001 else ss: set<$3670>.sizeck/set/size: (s : set<$3670>) -> int)

fun tree/foreachck/set/tree/foreach: forall<a,e> (t : tree<a>, action : (a) -> e ()) -> e ()(tt: tree<$3844>: treeck/set/tree: V -> V<aa: V>, actionaction: ($3844) -> $3845 (): aa: V -> ee: E (std/core/types/unit: V)std/core/types/unit: V)result: -> 3928 (): ee: E (std/core/types/unit: V)std/core/types/unit: V
  match tt: tree<$3844>
    Empck/set/Emp: forall<a> tree<a> -> (std/core/types/Unit: ())std/core/types/Unit: ()
    Brack/set/Bra: forall<a> (value : a, skew : skewness, left : tree<a>, right : tree<a>) -> tree<a>(vv: $3844, _, ll: tree<$3844>, rr: tree<$3844>) ->
      foreachck/set/tree/foreach: (t : tree<$3844>, action : ($3844) -> $3845 ()) -> $3845 ()(ll: tree<$3844>, actionaction: ($3844) -> $3845 ())
      actionaction: ($3844) -> $3845 ()(vv: $3844)
      foreachck/set/tree/foreach: (t : tree<$3844>, action : ($3844) -> $3845 ()) -> $3845 ()(rr: tree<$3844>, actionaction: ($3844) -> $3845 ())

// Iterate over elements in ascending order
pub fun foreachck/set/foreach: forall<a,e> (s : set<a>, action : (a) -> e ()) -> e ()(ss: set<$3795>: setck/set/set: V -> V<aa: V>, actionaction: ($3795) -> $3796 (): aa: V -> ee: E (std/core/types/unit: V)std/core/types/unit: V)result: -> 3843 (): ee: E (std/core/types/unit: V)std/core/types/unit: V
  ss: set<$3795>.treeck/set/set/tree: (set : set<$3795>) -> $3796 tree<$3795>.foreachck/set/tree/foreach: (t : tree<$3795>, action : ($3795) -> $3796 ()) -> $3796 ()(actionaction: ($3795) -> $3796 ())