def Auto.Lam2TH0.transLamBaseSort : Embedding.Lam.LamBaseSort → String

Equations

• Auto.Lam2TH0.transLamBaseSort Auto.Embedding.Lam.LamBaseSort.prop = "$o"
• Auto.Lam2TH0.transLamBaseSort Auto.Embedding.Lam.LamBaseSort.bool = "$o"
• Auto.Lam2TH0.transLamBaseSort Auto.Embedding.Lam.LamBaseSort.nat = "s_nat"
• Auto.Lam2TH0.transLamBaseSort Auto.Embedding.Lam.LamBaseSort.int = "s_int"
• Auto.Lam2TH0.transLamBaseSort (Auto.Embedding.Lam.LamBaseSort.isto0 Auto.Pos.xH) = "s_string"
• Auto.Lam2TH0.transLamBaseSort (Auto.Embedding.Lam.LamBaseSort.isto0 Auto.Pos.xH.xO) = "s_empty"
• Auto.Lam2TH0.transLamBaseSort (Auto.Embedding.Lam.LamBaseSort.isto0 p) = "s_empty"
• Auto.Lam2TH0.transLamBaseSort (Auto.Embedding.Lam.LamBaseSort.bv n) = toString "s_bv" ++ toString n ++ toString ""

def Auto.Lam2TH0.transLamSort : Embedding.Lam.LamSort → String

Equations

• Auto.Lam2TH0.transLamSort (Auto.Embedding.Lam.LamSort.atom n) = toString "s_a" ++ toString n ++ toString ""
• Auto.Lam2TH0.transLamSort (Auto.Embedding.Lam.LamSort.base b) = Auto.Lam2TH0.transLamBaseSort b
• Auto.Lam2TH0.transLamSort (s1.func s2) = toString "(" ++ toString (Auto.Lam2TH0.transLamSort s1) ++ toString " > " ++ toString (Auto.Lam2TH0.transLamSort s2) ++ toString ")"

def Auto.Lam2TH0.transPropConst : Embedding.Lam.PropConst → String

Equations

• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.trueE = "$true"
• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.falseE = "$false"
• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.not = "(~)"
• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.and = "(&)"
• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.or = "(|)"
• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.imp = "(=>)"
• Auto.Lam2TH0.transPropConst Auto.Embedding.Lam.PropConst.iff = "(=)"

def Auto.Lam2TH0.transBoolConst : Embedding.Lam.BoolConst → String

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2TH0.transBoolConst Auto.Embedding.Lam.BoolConst.trueb = "$true"
• Auto.Lam2TH0.transBoolConst Auto.Embedding.Lam.BoolConst.falseb = "$false"
• Auto.Lam2TH0.transBoolConst Auto.Embedding.Lam.BoolConst.notb = "(~)"
• Auto.Lam2TH0.transBoolConst Auto.Embedding.Lam.BoolConst.andb = "(&)"
• Auto.Lam2TH0.transBoolConst Auto.Embedding.Lam.BoolConst.orb = "(|)"

def Auto.Lam2TH0.transNatConst (nc : Embedding.Lam.NatConst) : String

Equations

• Auto.Lam2TH0.transNatConst nc = "t_" ++ nc.reprAux.replace " " "_"

def Auto.Lam2TH0.transIntConst (ic : Embedding.Lam.IntConst) : String

Equations

• Auto.Lam2TH0.transIntConst ic = "t_" ++ ic.reprAux

def Auto.Lam2TH0.transString (s : String) : String

Equations

• Auto.Lam2TH0.transString s = String.join (List.map (fun (c : Char) => toString "d" ++ toString c.toNat ++ toString "") s.data)

def Auto.Lam2TH0.transStringConst : Embedding.Lam.StringConst → String

Equations

• Auto.Lam2TH0.transStringConst (Auto.Embedding.Lam.StringConst.strVal s) = "t_strVal_" ++ Auto.Lam2TH0.transString s
• Auto.Lam2TH0.transStringConst x✝ = "t_" ++ x✝.reprAux

def Auto.Lam2TH0.transBitVecConst (bvc : Embedding.Lam.BitVecConst) : String

Equations

• Auto.Lam2TH0.transBitVecConst bvc = "t_" ++ bvc.reprAux.replace " " "_"

def Auto.Lam2TH0.transNatConstSort (nc : Embedding.Lam.NatConst) : String

Equations

• Auto.Lam2TH0.transNatConstSort nc = Auto.Lam2TH0.transLamSort nc.lamCheck

def Auto.Lam2TH0.transIntConstSort (ic : Embedding.Lam.IntConst) : String

Equations

• Auto.Lam2TH0.transIntConstSort ic = Auto.Lam2TH0.transLamSort ic.lamCheck

def Auto.Lam2TH0.transStringConstSort (sc : Embedding.Lam.StringConst) : String

Equations

• Auto.Lam2TH0.transStringConstSort sc = Auto.Lam2TH0.transLamSort sc.lamCheck

def Auto.Lam2TH0.transBitVecConstSort (bvc : Embedding.Lam.BitVecConst) : String

Equations

• Auto.Lam2TH0.transBitVecConstSort bvc = Auto.Lam2TH0.transLamSort bvc.lamCheck

def Auto.Lam2TH0.transLamBaseTerm : Embedding.Lam.LamBaseTerm → Except String String

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.pcst pc) = Except.ok (Auto.Lam2TH0.transPropConst pc)
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.bcst bc) = Except.ok (Auto.Lam2TH0.transBoolConst bc)
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.ncst nc) = Except.ok (Auto.Lam2TH0.transNatConst nc)
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.icst ic) = Except.ok (Auto.Lam2TH0.transIntConst ic)
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.scst sc) = Except.ok (Auto.Lam2TH0.transStringConst sc)
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.bvcst bvc) = Except.ok (Auto.Lam2TH0.transBitVecConst bvc)
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.ocst a) = Except.error "transLamBaseTerm :: attributes not supported in TPTP"
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.eqI a) = Except.error "transLamBaseTerm :: eqI should not occur here"
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.forallEI a) = Except.error "transLamBaseTerm :: forallEI should not occur here"
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.existEI a) = Except.error "transLamBaseTerm :: existEI should not occur here"
• Auto.Lam2TH0.transLamBaseTerm (Auto.Embedding.Lam.LamBaseTerm.iteI a) = Except.error "transLamBaseTerm :: iteI should not occur here"

partial def Auto.Lam2TH0.transLamTerm (t : Embedding.Lam.LamTerm) (lctx : Nat := 0) : Except String String

def Auto.Lam2TH0.transLamTerm.expandQuantBody (s : Embedding.Lam.LamSort) (t : Embedding.Lam.LamTerm) : Embedding.Lam.LamTerm

Equations

• Auto.Lam2TH0.transLamTerm.expandQuantBody s (Auto.Embedding.Lam.LamTerm.lam a body) = body
• Auto.Lam2TH0.transLamTerm.expandQuantBody s t = (Auto.Embedding.Lam.LamTerm.app s t (Auto.Embedding.Lam.LamTerm.bvar 0)).headBeta

partial def Auto.Lam2TH0.transLamTerm.transQuantApp (quant body : Embedding.Lam.LamTerm) (lctx : Nat) : Except String String