The answer( ) elaborator

This file provides syntax for marking up answers in a problem statement.

Note: certain problems also providing an answer, and can be formalised using answer(sorry) as a placeholder. While providing a proof simply requires finding any way to replace := sorry, providing an answer is not just finding any way to replace answer(sorry): it requires evaluation of mathematical meaning, which is a job for human mathematicians, not Lean alone.

def Google.answerElab : Lean.Elab.Term.TermElab

Indicates where the answer is in a problem statement.

Equations

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

structure Google.AnswerInfo : Type

An answer: a term, and the context in which it was elaborated

• ctx : Lean.Elab.ContextInfo
• term : Lean.Elab.TermInfo

def Google.AnswerInfo.format (a : AnswerInfo) : Lean.Elab.TermElabM Lean.MessageData

Print an answer

Equations

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

def Google.getAnswers {m : Type → Type u_1} [Monad m] (i : Lean.Elab.InfoTree) : m (Array AnswerInfo)

Find answers by inspecting an InfoTree

Equations

• Google.getAnswers i = Google.getAnswers.go none i

partial def Google.getAnswers.go {m : Type → Type u_1} [Monad m] : Option Lean.Elab.ContextInfo → Lean.Elab.InfoTree → m (Array AnswerInfo)