def CordialMiners.Tests.sampleDeps : ℕ → Finset ℕ

A small dependency graph: 2 and 3 each depend on 1, and 4 depends on both 2 and 3.

Equations

• CordialMiners.Tests.sampleDeps 2 = {1}
• CordialMiners.Tests.sampleDeps 3 = {1}
• CordialMiners.Tests.sampleDeps 4 = {2, 3}
• CordialMiners.Tests.sampleDeps x✝ = ∅

def CordialMiners.Tests.sampleSnapshot : CommitteeSnapshot ℕ

A test snapshot: three equal-weight members and a simple-majority threshold.

Equations

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

def CordialMiners.Tests.numDec : Sexpr → Option ℕ

A number codec for extraction: a Wave or Hash is just a number atom here, and parsing reads it back. It is a left inverse, so extraction round-trips.

Equations

• CordialMiners.Tests.numDec (CordialMiners.Sexpr.num n) = some n
• CordialMiners.Tests.numDec x✝ = none