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.

inductive Google.AnswerSetting : Type

A type that captures the current setting for the answer() elaborator.

• alwaysTrue : AnswerSetting

  Default mode: answer(sorry) defaults to True when sorry has type Prop.

• postpone : AnswerSetting

  Default mode for answer(foo): just postpones elaboration.

• withAuxiliary : AnswerSetting

  Elaborate answer(foo) by creating an auxiliary definition with value foo.

def Google.instInhabitedAnswerSetting.default : AnswerSetting

Equations

• Google.instInhabitedAnswerSetting.default = Google.AnswerSetting.alwaysTrue

instance Google.instInhabitedAnswerSetting : Inhabited AnswerSetting

Equations

• Google.instInhabitedAnswerSetting = { default := Google.instInhabitedAnswerSetting.default }

instance Google.instToJsonAnswerSetting : Lean.ToJson AnswerSetting

Equations

• Google.instToJsonAnswerSetting = { toJson := Google.instToJsonAnswerSetting.toJson }

def Google.instToJsonAnswerSetting.toJson : AnswerSetting → Lean.Json

Equations

• Google.instToJsonAnswerSetting.toJson Google.AnswerSetting.alwaysTrue = Lean.toJson "alwaysTrue"
• Google.instToJsonAnswerSetting.toJson Google.AnswerSetting.postpone = Lean.toJson "postpone"
• Google.instToJsonAnswerSetting.toJson Google.AnswerSetting.withAuxiliary = Lean.toJson "withAuxiliary"

def Google.instBEqAnswerSetting.beq : AnswerSetting → AnswerSetting → Bool

Equations

• Google.instBEqAnswerSetting.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Google.instBEqAnswerSetting : BEq AnswerSetting

Equations

• Google.instBEqAnswerSetting = { beq := Google.instBEqAnswerSetting.beq }

instance Google.instToStringAnswerSetting : ToString AnswerSetting

Equations

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

instance Google.instValueAnswerSetting : Lean.KVMap.Value AnswerSetting

Equations

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

opaque Google.google.answer : Lean.Option AnswerSetting

def Google.mkAnswerAnnotation (e : Lean.Expr) : Lean.Expr

Equations

• Google.mkAnswerAnnotation e = Lean.mkAnnotation `answer e

def Google.elabTermAndAnnotate (stx : Lean.TSyntax `term) (expectedType? : Option Lean.Expr) (postpone : Bool := false) : Lean.Elab.TermElabM Lean.Expr

Equations

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

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)