Skip to content

doc: clarify trust requirements on kernel#847

Draft
OrfeasLitos wants to merge 1 commit into
leanprover:mainfrom
OrfeasLitos:trusted-base
Draft

doc: clarify trust requirements on kernel#847
OrfeasLitos wants to merge 1 commit into
leanprover:mainfrom
OrfeasLitos:trusted-base

Conversation

@OrfeasLitos
Copy link
Copy Markdown
Contributor

Clarifies that trusting only the kernel needs manual inspection of the elaborated types.
The clarification is added as a footnote to "Kernel Checking". Authored after this Zulip discussion.

@OrfeasLitos OrfeasLitos marked this pull request as draft May 10, 2026 21:32
@OrfeasLitos OrfeasLitos changed the title Clarify trust requirements on kernel doc: clarify trust requirements on kernel May 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant