@[reducible, inline]

abbrev Perc : Type

Equations

• Perc = { i : Nat // 0 < i ∧ i ≤ 100 }

structure MidgardParameters : Type

• max_transfer_token_count : Nat
• shift_duration : Nat
• event_wait_duration : Nat
• maturity_duration : Nat
• registration_duration : Nat
• required_bond : Nat
• fraud_prover_reward : Perc
• slashing_penality : Perc

instance instReprMidgardParameters : Repr MidgardParameters

Equations

• instReprMidgardParameters = { reprPrec := instReprMidgardParameters.repr }

def instReprMidgardParameters.repr : MidgardParameters → Nat → Std.Format

Equations

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

def MidgardParameters.simple : MidgardParameters

Equations

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

structure MidgardHub : Type