Helpers to invoke functions involving algebra at tactic time

This file provides instances on x y : Q($α) such that x + y = q($x + $y).

def Expr.instOne {u : Lean.Level} (α : Q(Type u)) : Q(One «$α») → One Q(«$α»)

Produce a One instance for Q($α) such that 1 : Q($α) is q(1 : $α).

Equations

• Expr.instOne α x = { one := q(1) }

def Expr.instZero {u : Lean.Level} (α : Q(Type u)) : Q(Zero «$α») → Zero Q(«$α»)

Produce a Zero instance for Q($α) such that 0 : Q($α) is q(0 : $α).

Equations

• Expr.instZero α x = { zero := q(0) }

def Expr.instMul {u : Lean.Level} (α : Q(Type u)) : Q(Mul «$α») → Mul Q(«$α»)

Produce a Mul instance for Q($α) such that x * y : Q($α) is q($x * $y).

Equations

• Expr.instMul α x = { mul := fun (x_1 y : Q(«$α»)) => q(«$x_1» * «$y») }

def Expr.instAdd {u : Lean.Level} (α : Q(Type u)) : Q(Add «$α») → Add Q(«$α»)

Produce an Add instance for Q($α) such that x + y : Q($α) is q($x + $y).

Equations

• Expr.instAdd α x = { add := fun (x_1 y : Q(«$α»)) => q(«$x_1» + «$y») }