# Elaborator for functorial binary operators #

`fbinop% f x y`

elaborates `f x y`

for `x : S α`

and `y : S' β`

, taking into account
any coercions that the "functors" `S`

and `S'`

possess.

While `binop%`

tries to solve for a single minimal type, `fbinop%`

tries to solve
the parameterized problem of solving for a single minimal "functor."

The code is drawn from the Lean 4 core `binop%`

elaborator. Two simplifications made were

- It is assumed that every
`f`

has a "homogeneous" instance (think`Set.prod : Set α → Set β → Set (α × β)`

). - It is assumed that there are no "non-homogeneous" default instances.

It also makes the assumption that the binop wants to be as homogeneous as possible.
For example, when the type of an argument is unknown it will try to unify the argument's type
with `S _`

, which can help certain elaboration problems proceed (like for `{a,b,c}`

notation).

The main goal is to support generic set product notation and have it elaborate in a convenient way.

`fbinop% f x y`

elaborates `f x y`

for `x : S α`

and `y : S' β`

, taking into account
any coercions that the "functors" `S`

and `S'`

possess.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- FBinopElab.instInhabitedSRec = { default := { name := default, args := default } }

## Equations

- FBinopElab.instToExprSRec = { toExpr := FBinopElab.toExprSRec✝, toTypeExpr := Lean.Expr.const `FBinopElab.SRec [] }

## Equations

- FBinopElab.elabBinOp stx expectedType? = do let __do_lift ← FBinopElab.toTree stx FBinopElab.toExpr __do_lift expectedType?