module Numbers {
  inline func ++(x: Int, y: Int) returns (r: Int) { x + y }

  inline func _[_.._](s: Int, lo: Int, hi: Int) returns (r: Int) {
    s + lo + hi
  }
}

module NumbersClient {
  import Numbers.++
  import Numbers._[_.._]

  lemma examples() {
    assert 1 ++ 2 == 3;
    assert (1 ++ 2) == Numbers.++(1, 2);
    assert 10[1..3] == 14;
    assert 10[1..3] == Numbers._[_.._](10, 1, 3);
  }
}

module Keys: Library.OrderedType {
  rep type T = data { case key(value: Int) }

  func <(x: T, y: T) returns (r: Bool) { x.value < y.value }
}

module OrderedClient {
  import Keys._

  lemma examples() {
    val a := key(1);
    val b := key(2);
    assert a < b && a <= b;
    assert (a < b) == Keys.<(a, b);
    assert a <= a;
    assert 0 < 1 <= 2;
  }
}

module SingleEntry {
  rep type T = data { case entry(value: Int) }

  inline func _[_](s: T, i: Int) returns (r: Int) {
    i == 0 ? s.value : 0
  }

  inline func _[_:=_](s: T, i: Int, e: Int) returns (r: T) {
    i == 0 ? entry(e) : s
  }
}

module UpdateClient {
  import SingleEntry._

  lemma examples() {
    var s := entry(1);
    assert s[0] == SingleEntry._[_](s, 0);
    assert s[0] == 1;
    assert s[0 := 2] == SingleEntry._[_:=_](s, 0, 2);
    s[0] := 2;
    assert s == entry(2) && s[0] == 2;
    assert s[1 := 3] == s;

    var m: Map[Int, Int] := { i: Int :: 0 };
    m[1] := 3;
    assert m[1] == 3;
    assert _[_:=_](m, 2, 4) == m[2 := 4];
  }
}

module Symbols {
  inline func +?(x: Int, y: Int) returns (r: Int) { 10 * x + y }
  inline func +:(x: Int, y: Int) returns (r: Int) { 10 * x + y }
}

module SymbolsClient {
  import Symbols._

  lemma examples() {
    assert 1 +? 2 * 3 == 16;
    assert 1 +? 2 +? 3 == 123;
    assert 1 +: 2 +: 3 == 33;
    assert (1 +? 2) == Symbols.+?(1, 2);
  }
}