inductive SExp (O : Type uo) (N : Type un) : Type (max un uo)

• var {O : Type uo} {N : Type un} : N → SExp O N
• op {O : Type uo} {N : Type un} : O → {arity : ℕ} → (Fin arity → SExp O N) → SExp O N

def SExp.mapOp {O : Type u_1} {O' : Type u_2} {N : Type u_3} (f : O → O') : SExp O N → SExp O' N

Equations

• SExp.mapOp f (SExp.var n) = SExp.var n
• SExp.mapOp f (SExp.op o es) = SExp.op (f o) fun (i : Fin arity) => SExp.mapOp f (es i)

def SExp.mapVar {O : Type u_1} {N : Type u_2} {N' : Type u_3} (f : N → N') : SExp O N → SExp O N'

Equations

• SExp.mapVar f (SExp.var n) = SExp.var (f n)
• SExp.mapVar f (SExp.op o es) = SExp.op o fun (i : Fin arity) => SExp.mapVar f (es i)

def SExp.bindOp {O : Type u_1} {O' : Type u_2} {N : Type u_3} (interpOp : O → {arity : ℕ} → (Fin arity → SExp O' N) → SExp O' N) : SExp O N → SExp O' N

Equations

• SExp.bindOp interpOp (SExp.var n) = SExp.var n
• SExp.bindOp interpOp (SExp.op o es) = interpOp o fun (i : Fin arity) => SExp.bindOp interpOp (es i)

@[simp]

theorem SExp.bindOp_pure {O : Type u_1} {N : Type u_2} (e : SExp O N) : bindOp op e = e

def SExp.bindVar {O : Type u_1} {N : Type u_2} {N' : Type u_3} (interpVar : N → SExp O N') : SExp O N → SExp O N'

Equations

• SExp.bindVar interpVar (SExp.var n) = interpVar n
• SExp.bindVar interpVar (SExp.op o es) = SExp.op o fun (i : Fin arity) => SExp.bindVar interpVar (es i)

@[simp]

theorem SExp.bindVar_pure {O : Type u_1} {N : Type u_2} (e : SExp O N) : bindVar var e = e

inductive SExpL.Kind : Type

• sexp : Kind
• list : Kind

inductive SExpL (O : Type uo) (N : Type un) : SExpL.Kind → Type (max un uo)

• var {O : Type uo} {N : Type un} : N → SExpL O N Kind.sexp
• op {O : Type uo} {N : Type un} : O → SExpL O N Kind.list → SExpL O N Kind.sexp
• nil {O : Type uo} {N : Type un} : SExpL O N Kind.list
• cons {O : Type uo} {N : Type un} : SExpL O N Kind.sexp → SExpL O N Kind.list → SExpL O N Kind.list

def SExpL.Kind.toSExp (O : Type uo) (N : Type un) : Kind → Type (max uo un)

Equations

• SExpL.Kind.toSExp O N SExpL.Kind.sexp = SExp O N
• SExpL.Kind.toSExp O N SExpL.Kind.list = List (SExp O N)

@[irreducible]

def SExpL.toList {O : Type u_1} {N : Type u_2} : SExpL O N Kind.list → List (SExpL O N Kind.sexp)

Equations

• SExpL.nil.toList = []
• (e.cons es).toList = e :: es.toList

def SExpL.toSExp {O : Type u_1} {N : Type u_2} {k : Kind} : SExpL O N k → Kind.toSExp O N k

Equations

• (SExpL.var n).toSExp = SExp.var n
• (SExpL.op o es).toSExp = SExp.op o (List.get es.toSExp)
• SExpL.nil.toSExp = []
• (e.cons es).toSExp = e.toSExp :: es.toSExp