ToExpr instances for AC types.

def Lean.Meta.Grind.AC.ofSeq (m : Grind.AC.Seq) : Expr

Equations

• Lean.Meta.Grind.AC.ofSeq (Lean.Grind.AC.Seq.var x) = Lean.mkApp (Lean.mkConst `Lean.Grind.AC.Seq.var) (Lean.toExpr x)
• Lean.Meta.Grind.AC.ofSeq (Lean.Grind.AC.Seq.cons x s) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.AC.Seq.cons) (Lean.toExpr x) (Lean.Meta.Grind.AC.ofSeq s)

instance Lean.Meta.Grind.AC.instToExprSeq : ToExpr Grind.AC.Seq

Equations

• Lean.Meta.Grind.AC.instToExprSeq = { toExpr := Lean.Meta.Grind.AC.ofSeq, toTypeExpr := Lean.mkConst `Lean.Grind.AC.Seq }

def Lean.Meta.Grind.AC.ofExpr (m : Grind.AC.Expr) : Expr

Equations

• Lean.Meta.Grind.AC.ofExpr (Lean.Grind.AC.Expr.var x) = Lean.mkApp (Lean.mkConst `Lean.Grind.AC.Expr.var) (Lean.toExpr x)
• Lean.Meta.Grind.AC.ofExpr (lhs.op rhs) = Lean.mkApp2 (Lean.mkConst `Lean.Grind.AC.Expr.op) (Lean.Meta.Grind.AC.ofExpr lhs) (Lean.Meta.Grind.AC.ofExpr rhs)

instance Lean.Meta.Grind.AC.instToExprExpr : ToExpr Grind.AC.Expr

Equations

• Lean.Meta.Grind.AC.instToExprExpr = { toExpr := Lean.Meta.Grind.AC.ofExpr, toTypeExpr := Lean.mkConst `Lean.Grind.AC.Expr }