The standard description may be found at this address:
archetype erc20constant total : nat = 1_000_000_000_000_000variable onetoken : nat = 1_000_000asset allowance identified by owner spender {owner : address;spender : address;amount : nat;}asset tokenHolder identified by holder {holder : address;tokens : nat = 0;} initialized by {{ holder = caller; tokens = total }}entry dotransfer (dest : pkey<tokenHolder>, value : nat) {require {d0 : tokenHolder[caller].tokens >= value}effect {tokenHolder.addupdate( dest, { tokens += value });tokenHolder.update( caller, { tokens -= value })}}entry approve(ispender : address, value : nat) {require {d1 : tokenHolder[caller].tokens >= value;}effect {allowance.addupdate((caller, ispender), { amount = value });}}entry transferFrom(from_ : address, to_ : address, value : nat) {require {(* d1: allowance.contains(from_); *)d3: allowance[(from_,caller)].amount >= value;d4: tokenHolder[from_].tokens >= value}effect {(* update allowance *)allowance.update((from_,caller), { amount -= value });(* update token *)tokenHolder.addupdate(to_, { tokens += value });tokenHolder.update(from_, { tokens -= value });}}