inductive Network : Type

• Mainnet : Network
• Testnet : Network

@[reducible, inline]

abbrev Coin : Type

Equations

• Coin = Nat

@[reducible, inline]

abbrev Address : Type

Equations

• Address = String

@[reducible, inline]

abbrev Value : Type

Equations

• Value = Nat

@[reducible, inline]

abbrev Data : Type

Equations

• Data = String

@[reducible, inline]

abbrev TxId : Type

Equations

• TxId = Nat

@[reducible, inline]

abbrev VKeyHash : Type

Equations

• VKeyHash = Nat