@[reducible, inline]

abbrev Tokens.Elem.TId : Type

Equations

• Tokens.Elem.TId = Nat

We simulate having blockchain tokens as elements having a name, some data and an id.

structure Tokens.Elem.TokenD (α : Type) : Type

• name : Unit
• data : α
• id : TId

instance Tokens.Elem.instReprTokenD {α✝ : Type} [Repr α✝] : Repr (TokenD α✝)

Equations

• Tokens.Elem.instReprTokenD = { reprPrec := Tokens.Elem.instReprTokenD.repr }

def Tokens.Elem.instReprTokenD.repr {α✝ : Type} [Repr α✝] : TokenD α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.