// Integer set
module set

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

// Sets of integers.
// Duplicates are omitted
abstract type setck/set/set: V
  Empck/set/Emp: set
  Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set{ valuevalue: int: intstd/core/types/int: V; skewskew: skewness: skewnessck/set/skewness: V; leftleft: set: setck/set/set: V; rightright: set: setck/set/set: V }

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

pub fun showck/set/show.1: (t : set) -> string(tt: set: setck/set/set: V): stringstd/core/types/string: V
  match tt: set
    Empck/set/Emp: set -> "Emp"
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(vv: int, ss: skewness, ll: set, rr: set) ->
      "Bra(" ++std/core/(++).1: (x : string, y : string) -> string vv: int.showstd/core/show: (i : int) -> string ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string ss: skewness.showck/set/show: (s : skewness) -> string ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string ll: set.showck/set/show.1: (t : set) -> string ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string rr: set.showck/set/show.1: (t : set) -> string ++std/core/(++).1: (x : string, y : string) -> string ")"

// Check whether a set is empty
pub fun is-emptyck/set/is-empty: (t : set) -> bool(tt: set: setck/set/set: V): boolstd/core/types/bool: V
  match tt: set
    Empck/set/Emp: set -> Truestd/core/types/True: bool
    _ -> Falsestd/core/types/False: bool

// Create an empty set
pub fun emptyck/set/empty: () -> set(): setck/set/set: V
  Empck/set/Emp: set

// Create a set with a single element
pub fun singletonck/set/singleton: (v : int) -> set(vv: int: intstd/core/types/int: V)
  Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set( value = vv: int, skew = Eck/set/E: skewness, left = Empck/set/Emp: set, right = Empck/set/Emp: set )

// Check whether a value belongs to a set
pub fun memck/set/mem: (t : set, v : int) -> bool(tt: set: setck/set/set: V, vv: int: intstd/core/types/int: V): boolstd/core/types/bool: V
  match tt: set
    Empck/set/Emp: set -> Falsestd/core/types/False: bool
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, _, _, _) | vv: int ==std/core/(==).1: (x : int, y : int) -> bool aa: int -> Truestd/core/types/True: bool
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, _, ll: set, _) | vv: int <std/core/(<).1: (x : int, y : int) -> bool aa: int -> ll: set.memck/set/mem: (t : set, v : int) -> bool(vv: int)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(_, _, _, rr: set) -> rr: set.memck/set/mem: (t : set, v : int) -> bool(vv: int)

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

fun adjust-rck/set/adjust-r: (t : set) -> (set, bool)(tt: set: setck/set/set: V): (std/core/types/(,): (V, V) -> Vsetck/set/set: V, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  match tt: set
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Lck/set/L: skewness, ll: set, rr: set) -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Eck/set/E: skewness, ll: set, rr: set), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Eck/set/E: skewness, ll: set, rr: set) -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, rr: set), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Rck/set/R: skewness, l'l': set, r'r': set)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Eck/set/E: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Eck/set/E: skewness, ll: set, l'l': set), r'r': set), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Eck/set/E: skewness, l'l': set, r'r': set)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Lck/set/L: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, l'l': set), r'r': set), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Lck/set/L: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(cc: int, Lck/set/L: skewness, l''l'': set, r''r'': set), r'r': set)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(cc: int, Eck/set/E: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Eck/set/E: skewness, ll: set, l''l'': set), Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Rck/set/R: skewness, r''r'': set, r'r': set)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Lck/set/L: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(cc: int, Eck/set/E: skewness, l''l'': set, r''r'': set), r'r': set)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(cc: int, Eck/set/E: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Eck/set/E: skewness, ll: set, l''l'': set), Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Eck/set/E: skewness, r''r'': set, r'r': set)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Rck/set/R: skewness, ll: set, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Lck/set/L: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(cc: int, Rck/set/R: skewness, l''l'': set, r''r'': set), r'r': set)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(cc: int, Eck/set/E: skewness, Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, Lck/set/L: skewness, ll: set, l''l'': set), Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(bb: int, Eck/set/E: skewness, r''r'': set, r'r': set)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    _ -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)tt: set, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) // for exhaustive check

// insert-intl(t, v) = (t', grown)
//    t' : t に v を挿入して得られる木
// grown : 高さが 1 増えたか
fun insert-intlck/set/insert-intl: (t : set, v : int) -> (set, bool)(tt: set: setck/set/set: V, vv: int: intstd/core/types/int: V): (std/core/types/(,): (V, V) -> Vsetck/set/set: V, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  match tt: set
    Empck/set/Emp: set -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)singletonck/set/singleton: (v : int) -> set(vv: int), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, _, _, _) | vv: int ==std/core/(==).1: (x : int, y : int) -> bool aa: int -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)tt: set, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) // v がすでに存在するときは追加しない
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, ll: set, rr: set) | vv: int <std/core/(<).1: (x : int, y : int) -> bool aa: int ->
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)l'l': set, growngrown: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = ll: set.insert-intlck/set/insert-intl: (t : set, v : int) -> (set, bool)(vv: int)
      val t't': set = Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, l'l': set, rr: set)
      if !std/core/types/(!).1: (b : bool) -> boolgrowngrown: bool then returnreturn: (set, bool) (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t't': set, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
      t't': set.adjust-lck/set/adjust-l: (t : set) -> (set, bool)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, ll: set, rr: set) ->
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)r'r': set, growngrown: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = rr: set.insert-intlck/set/insert-intl: (t : set, v : int) -> (set, bool)(vv: int)
      val t't': set = Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, ll: set, r'r': set)
      if !std/core/types/(!).1: (b : bool) -> boolgrowngrown: bool then returnreturn: (set, bool) (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t't': set, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
      t't': set.adjust-rck/set/adjust-r: (t : set) -> (set, bool)

// Add a value to a set.
// Do nothing if the given value already exists
pub fun insertck/set/insert: (t : set, v : int) -> set(tt: set: setck/set/set: V, vv: int: intstd/core/types/int: V): setck/set/set: V
  tt: set.insert-intlck/set/insert-intl: (t : set, v : int) -> (set, bool)(vv: int).fststd/core/types/fst: forall<a,b> ((a, b)) -> a

// Return the minimum element of a set
pub fun minck/set/min: (t : set) -> maybe<int>(tt: set: setck/set/set: V): maybestd/core/types/maybe: V -> V<intstd/core/types/int: V>
  match tt: set
    Empck/set/Emp: set -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, _, Empck/set/Emp: set, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(aa: int)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(_, _, ll: set, _) -> ll: set.minck/set/min: (t : set) -> maybe<int>

// Return the maximum element of a set
pub fun maxck/set/max: (t : set) -> maybe<int>(tt: set: setck/set/set: V): maybestd/core/types/maybe: V -> V<intstd/core/types/int: V>
  match tt: set
    Empck/set/Emp: set -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, _, _, Empck/set/Emp: set) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(aa: int)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(_, _, _, rr: set) -> rr: set.maxck/set/max: (t : set) -> maybe<int>

// erase-intl(t, v) = (t', deleted, shrinked)
//          t' : t から v をなくした木
//     deleted : v を削除したか (元からなければ false)
//    shrinked : 高さが 1 減ったか
fun erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(tt: set: setck/set/set: V, vv: int: intstd/core/types/int: V): (std/core/types/(,,): (V, V, V) -> Vsetck/set/set: V, boolstd/core/types/bool: V, boolstd/core/types/bool: V)std/core/types/(,,): (V, V, V) -> V
  match tt: set
    Empck/set/Emp: set -> (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/set/Emp: set, Falsestd/core/types/False: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, ll: set, rr: set) | vv: int <std/core/(<).1: (x : int, y : int) -> bool aa: int ->
      val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': set, deleteddeleted: bool, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: set.erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(vv: int)
      val t't': set = Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, l'l': set, rr: set)
      if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (set, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': set, deleteddeleted: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': set, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': set.adjust-rck/set/adjust-r: (t : set) -> (set, bool)
      (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': set, deleteddeleted: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, ll: set, rr: set) | vv: int >std/core/(>).1: (x : int, y : int) -> bool aa: int ->
      val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': set, deleteddeleted: bool, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: set.erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(vv: int)
      val t't': set = Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(aa: int, ss: skewness, ll: set, r'r': set)
      if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (set, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': set, deleteddeleted: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': set, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': set.adjust-lck/set/adjust-l: (t : set) -> (set, bool)
      (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': set, deleteddeleted: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(_, ss: skewness, ll: set, rr: set) ->
      match rr: set.minck/set/min: (t : set) -> maybe<int>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(mnmn: int) ->
          val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': set, _, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: set.erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(mnmn: int)
          val t't': set = Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(mnmn: int, ss: skewness, ll: set, r'r': set)
          if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (set, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': set, Truestd/core/types/True: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
          val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': set, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': set.adjust-lck/set/adjust-l: (t : set) -> (set, bool)
          returnreturn: (set, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': set, Truestd/core/types/True: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
        _ -> (std/core/types/(): ())std/core/types/(): ()
      match ll: set.maxck/set/max: (t : set) -> maybe<int>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(mxmx: int) ->
          val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': set, _, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: set.erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(mxmx: int)
          val t't': set = Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(mxmx: int, ss: skewness, l'l': set, rr: set)
          if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (set, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': set, Truestd/core/types/True: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
          val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': set, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': set.adjust-rck/set/adjust-r: (t : set) -> (set, bool)
          returnreturn: (set, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': set, Truestd/core/types/True: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
        _ -> (std/core/types/(): ())std/core/types/(): ()
      (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/set/Emp: set, Truestd/core/types/True: bool, Truestd/core/types/True: bool)std/core/types/(,,): 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
pub fun eraseck/set/erase: (t : set, v : int) -> set(tt: set: setck/set/set: V, vv: int: intstd/core/types/int: V): setck/set/set: V
  tt: set.erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(vv: int).fststd/core/types/fst.1: forall<a,b,c> ((a, b, c)) -> a

pub fun erase-with-statusck/set/erase-with-status: (t : set, v : int) -> (set, bool)(tt: set: setck/set/set: V, vv: int: intstd/core/types/int: V): (std/core/types/(,): (V, V) -> Vsetck/set/set: V, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': set, deleteddeleted: bool, _)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = tt: set.erase-intlck/set/erase-intl: (t : set, v : int) -> (set, bool, bool)(vv: int)
  (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t't': set, deleteddeleted: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)

// Iterate over elements in ascending order
pub fun foreachck/set/foreach: forall<e> (t : set, action : (int) -> e ()) -> e ()(tt: set: setck/set/set: V, actionaction: (int) -> $959 (): intstd/core/types/int: V -> ee: E (std/core/types/(): V)std/core/types/(): V): ee: E (std/core/types/(): V)std/core/types/(): V
  match tt: set
    Empck/set/Emp: set -> (std/core/types/(): ())std/core/types/(): ()
    Brack/set/Bra: (value : int, skew : skewness, left : set, right : set) -> set(vv: int, _, ll: set, rr: set) ->
      foreachck/set/foreach: forall<e> (t : set, action : (int) -> e ()) -> e ()(ll: set, actionaction: (int) -> $959 ())
      actionaction: (int) -> $959 ()(vv: int)
      foreachck/set/foreach: forall<e> (t : set, action : (int) -> e ()) -> e ()(rr: set, actionaction: (int) -> $959 ())