Documentation

Lean.Elab.BindersUtil

def Lean.Elab.Term.expandOptType (ref : Lean.Syntax) (optType : Lean.Syntax) :

Equations

Lean.Elab.Term.expandOptType ref optType = if Lean.Syntax.isNone optType = true then Lean.mkHole ref else Lean.Syntax.getOp (Lean.Syntax.getOp optType 0) 1