From 8424fbbc3b0b9f9a2303dbbb8fd6c871cc870e91 Mon Sep 17 00:00:00 2001 From: Orfeas Stefanos Thyfronitis Litos Date: Sun, 10 May 2026 22:20:11 +0100 Subject: [PATCH] Clarify trust requirements on kernel --- Manual/Elaboration.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index c81e7a7eb..d3db0965b 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -99,7 +99,8 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol : Kernel Checking - Lean's trusted kernel checks the output of the elaborator to ensure that it follows the rules of the type theory. + Lean's trusted kernel{margin}[To avoid trusting the elaborator when verifying a statement, one has to {keywordOf Lean.Parser.Command.print}`#print` the statement to get the elaborated type and manually verify that it expresses the desired statement. + This brings {keywordOf Lean.Parser.Command.print}`#print` into the trusted base.] checks the output of the elaborator to ensure that it follows the rules of the type theory. : Compilation