ticket

let create: <a>(_: a) => (_: nat) => option<ticket<a>>

The call create(v, a) creates a ticket with value v and amount a. If the creation is a success, the value Some(t) is returned, where t is the ticket; otherwise, None() is the result. Note: Tickets cannot be duplicated.

let split: <a>(_: ticket<a>) => (_: [nat, nat]) => option<[ticket<a>, ticket<a>]>

The call split(t, [a1, a2]) results in a pair of tickets t1 and t2 such that the former owns the amount a1 and the later a2. More precisely, the value of the call is Some([t1, t2]) because signifying to the callee the failure of the splitting is achieved by returning the value None().

let join: <a>(_: [ticket<a>, ticket<a>]) => option<ticket<a>>

The call join(t1, t2) joins the tickets t1 and t2, which must have the same type of value.

let read: <a>(_: ticket<a>) => [[address, [a, nat]], ticket<a>]

The call read(t) returns t itself and the contents of t which is a pair [address, [value, amount]], where address is the address of the smart contract that created it.