Additions to "Try this" support

This file could be upstreamed to Std.

def addHaveSuggestion (ref : Lean.Syntax) (t? : Option Lean.Expr) (e : Lean.Expr) (origSpan? : optParam (Option Lean.Syntax) none) : Lean.Elab.TermElabM Unit

Add a suggestion for have : t := e.

Equations

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

def addRewriteSuggestion (ref : Lean.Syntax) (rules : List (Lean.Expr × Bool)) (type? : optParam (Option Lean.Expr) none) (loc? : optParam (Option Lean.Expr) none) (origSpan? : optParam (Option Lean.Syntax) none) : Lean.Elab.TermElabM Unit

Add a suggestion for rw [h₁, ← h₂] at loc.

Equations

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