Documentation

Mathlib.Tactic.TryThis

Additions to "Try this" support #

This file could be upstreamed to Std.

source
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.

Instances For
    source
    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.

    Instances For