Documentation

Lean.Meta.Tactic.Grind.AC.ToExpr

← Copula mathematical handbook

ToExpr instances for AC types.

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

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)

Instances For

@[instance_reducible]

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) :

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)

Instances For

@[instance_reducible]

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 }