inductive CordialMiners.Sexpr : Type

A MeTTaIL atom: a symbol, a natural-number literal, or an application (a list of atoms). This is the S-expression target the protocol facts extract into.

• sym : String → Sexpr
• num : Nat → Sexpr
• app : List Sexpr → Sexpr

partial def CordialMiners.instReprSexpr.repr : Sexpr → Nat → Std.Format

@[implicit_reducible]

instance CordialMiners.instReprSexpr : Repr Sexpr

Equations

• CordialMiners.instReprSexpr = { reprPrec := CordialMiners.instReprSexpr.repr }

@[implicit_reducible]

instance CordialMiners.instInhabitedSexpr : Inhabited Sexpr

Equations

• CordialMiners.instInhabitedSexpr = { default := CordialMiners.instInhabitedSexpr.default }