def Lean.Meta.Sym.getMaxFVar? (e : Expr) : SymM (Option FVarId)

Returns the maximal free variable occurring in e. This function assumes the current local context contains all free variables used in e.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.fvar fvarId) = pure (some fvarId)
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.const declName us) = pure none
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.bvar deBruijnIndex) = pure none
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.sort u) = pure none
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.lit a) = pure none
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.proj typeName idx s) = Lean.Meta.Sym.check✝ (Lean.Expr.proj typeName idx s) (Lean.Meta.Sym.getMaxFVar? s)
• Lean.Meta.Sym.getMaxFVar? (Lean.Expr.mdata data e_2) = Lean.Meta.Sym.check✝ e_2 (Lean.Meta.Sym.getMaxFVar? e_2)