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

1. It is assumed that every f has a "homogeneous" instance (think Set.prod : Set α → Set β → Set (α × β)).
2. 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.

def FBinopElab.prodSyntax : Lean.ParserDescr

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.

structure FBinopElab.SRec : Type

Records a "functor", which is some function Type u → Type v. We only allow c a1 ... an for c a constant. This is so we can abstract out the universe variables.

• name : Lean.Name
• args : Array Lean.Expr

instance FBinopElab.instInhabitedSRec : Inhabited FBinopElab.SRec

Equations

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

instance FBinopElab.instToExprSRec : Lean.ToExpr FBinopElab.SRec

Equations

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

def FBinopElab.elabBinOp : Lean.Elab.Term.TermElab

Equations

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