Utilities for creating and recognizing sorry

This module develops material for creating and recognizing sorryAx terms that encode originating source positions. There are three orthogonal configurations for sorries:

• The sorry could be synthetic. When elaboration fails on some subterm, then we can use a sorry to fill in the missing subterm. In this case elaboration marks the sorry as being "synthetic" while logging an error. The presence of synthetic sorries tends to suppress further errors. For example, the "this declaration contains sorry" error is not triggered for synthetic sorries as we assume there is already an error message logged.

• The sorry could be unique. A unique sorry is not definitionally equal to any other sorry, even if they have the same type. Normally sorryAx α s = sorryAx α s is a definitional equality. Unique sorries insert a unique tag t using the encoding sorryAx (τ → α) s t.

• The sorry could be labeled. A labeled sorry contains source position information, supporting the LSP "go to definition" feature in the Infoview, and also supporting pretty printing the sorry with an indication of source position when the option pp.sorrySource is true.

def Lean.Meta.mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr

Returns sorryAx type synthetic. Recall that synthetic is true if this sorry is from an error.

See also Lean.Meta.mkLabeledSorry, for creating a sorry that is labeled or unique.

Equations

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

structure Lean.Meta.SorryLabelView : Type

• module? : Option DeclarationLocation

  Records the origin module name, logical source position, and LSP range for the sorry. The logical source position is used when displaying the sorry when the pp.sorrySource option is true, and the LSP range is used for "go to definition" in the Infoview.

def Lean.Meta.SorryLabelView.encode (view : SorryLabelView) : CoreM Name

Equations

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

def Lean.Meta.SorryLabelView.decode? (name : Name) : Option SorryLabelView

Equations

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

def Lean.Meta.mkLabeledSorry (type : Expr) (synthetic unique : Bool) : MetaM Expr

Constructs a sorryAx.

• If the current ref has a source position, then creates a labeled sorry. This supports "go to definition" in the InfoView and pretty printing a source position when the pp.sorrySource option is true.
• If synthetic is true, then the sorry is regarded as being generated by the elaborator. The caller should ensure that there is an associated error logged.
• If unique is true, the sorry is unique, in the sense that it is not defeq to any other sorry created by mkLabeledSorry.

Equations

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

def Lean.Meta.isLabeledSorry? (e : Expr) : Option SorryLabelView

Returns a SorryLabelView if e is an application of an expression returned by mkLabeledSorry. If it is, then the sorry takes the first three arguments, and the tag is at argument 3.

Equations

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

def Lean.Expr.getSorry? (e : Expr) : Option Expr

If e is a sorry application, returns the sorry itself, stripping off any arguments in case the sorry is standing in for a function.

For labeled sorries, includes the label information.

Equations

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

def Lean.Meta.forEachSorryM {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr) (fn : Expr → m Unit) : m Unit

Evaluates fn on each sorry in the expression. Instantiates bound variables with free variables.

Equations

• Lean.Meta.forEachSorryM input fn = Lean.Meta.forEachExpr' input fun (e : Lean.Expr) => match e.getSorry? with | some e' => do fn e' pure false | x => pure true

def Lean.Declaration.forEachSorryM {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (decl : Declaration) (fn : Expr → m Unit) : m Unit

Evaluates fn on each sorry in the declaration.

Equations

• decl.forEachSorryM fn = decl.forExprM fun (x : Lean.Expr) => Lean.Meta.forEachSorryM x fn