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.findAnswerExpr (e : Lean.Expr) : Option Lean.Expr

Find the first subexpression carrying the answer annotation, returning the inner (unwrapped) expression if found.

Equations

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

def Google.findAnswerExprs (e : Lean.Expr) : Array Lean.Expr

Collect all subexpressions carrying the answer annotation, returning the inner (unwrapped) expressions.

Equations

• Google.findAnswerExprs e = Google.findAnswerExprs.go✝ 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.mkCanonicalSorryAnnotation (expectedType : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Construct a canonical sorryAx application with a stable, module-independent tag. Unlike Lean's built-in sorry macro, this does not embed the current module name via hygiene, so the resulting expression is identical regardless of whether the file is compiled as Challenge or Solution.

Equations

• Google.mkCanonicalSorryAnnotation expectedType = do let sorryExpr ← liftM (Lean.Meta.mkSorry expectedType false) pure (Google.mkAnswerAnnotation sorryExpr)

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