chaining expressions with arrows

Stream: lean4

[Arthur Paulino]

Suppose I have es : Array Expr. How build an Expr for es₁ → es₂ → ⋯?

[Edward Ayers]

To make a single arrow you can use Lean.mkForall, or Lean.Meta.mkArrow. I think for multiple you want Lean.Meta.mkForallFVars, which also does some bookkeeping for metavariables.