doc: mention that inferType does not ensure type correctness
#5087
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
hargoniX
reviewed
Aug 18, 2024
src/Lean/Meta/Basic.lean
Outdated
| /-- | ||
| Returns the inferred type of the given expression. | ||
|
|
||
| The type inference algorithm assumes the expression is type-correct for efficiency, |
There was a problem hiding this comment.
Could you maybe provide an example for a term that it might succeed on but provide a wrong result? This claim probably sounds quite fancy if you are used to the academic notion of "if type inference succeeds the type it returns is right"
There was a problem hiding this comment.
Thanks, I've added some examples of both accidental success and necessary failure.
leodemoura
reviewed
Aug 20, 2024
|
|
||
| The type inference algorithm does not do general type checking, | ||
| which is instead handled by the `Lean.Meta.check` algorithm. | ||
| Type inference only looks at subterms that are necessary for determining an expression's type, |
There was a problem hiding this comment.
It may be worth mentioning that we do not guarantee that Lean.Meta.check is as efficient and complete as the check implemented in the kernel.
There was a problem hiding this comment.
Thanks, I've moved the mention of Lean.Meta.check to a new paragraph with a comment about the kernel.
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 20, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 20, 2024
leanprover-community-mathlib4-bot
added
the
builds-mathlib
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
kmill
force-pushed
the
inferType_doc_update
branch
from
0330a2f to
9380611
Compare
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Sep 16, 2024
…rover#5087) This also adds links to the implementations of `whnf` and `inferType` to make it easier to navigate this part of the code base.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This also adds links to the implementations of
whnfandinferTypeto make it easier to navigate this part of the code base.