Skip to content

doc: fix error explanation wording #730

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
alok wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

doc: fix error explanation wording #730

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Manual/ErrorExplanations/InferDefTypeFailed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ ambiguities that may be contributing to this error.
Note that when an explicit resulting type is provided—even if that type contains holes—Lean will not
use information from the definition body to help infer the type of the definition or its parameters.
Thus, adding an explicit resulting type may also necessitate adding type annotations to parameters
whose types were previously inferrable. Additionally, it is always necessary to provide an explicit
whose types were previously inferable. Additionally, it is always necessary to provide an explicit
type in a `theorem` declaration: the `theorem` syntax requires a type annotation, and the elaborator
will never attempt to use the theorem body to infer the proposition being proved.

Expand Down
2 changes: 1 addition & 1 deletion Manual/ErrorExplanations/InvalidField.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ def double_plus_one (x : Nat) :=
(x + x).succ
```

The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation
The `Add` type class is sufficient for performing the addition `x + x`, but the `.succ` field notation
cannot operate without knowing more about the actual type from which `succ` is being projected.
:::

Expand Down
2 changes: 1 addition & 1 deletion Manual/ErrorExplanations/SynthInstanceFailed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ variable {t : Type} (x y : Int)

{ref "type-classes"}[Type classes] are the mechanism that Lean and many other
programming languages use to handle overloaded operations. The code that handles a particular
overloaded operation is an {tech}_instance_ of a typeclass; deciding which instance to use for a given
overloaded operation is an {tech}_instance_ of a type class; deciding which instance to use for a given
overloaded operation is called _synthesizing_ an instance.

As an example, when Lean encounters an expression {lean}`x + y` where {lean}`x` and {lean}`y` both
Expand Down
2 changes: 1 addition & 1 deletion Manual/Meta/ErrorExplanation/Header.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ def errorExplanationHeader : Verso.Doc.Elab.BlockCommandOf ErrorHeaderConfig
| cfg, _contents => do
match ← getErrorExplanation? cfg.name with
| .none =>
Lean.logWarning m!"The named error `{cfg.name}` is not not known by the Lean compiler"
Lean.logWarning m!"The named error `{cfg.name}` is not known by the Lean compiler"
let metadata := ErrorExplanationExtendedMetadata.mk (ErrorExplanation.Metadata.mk "Summary unavailable" "Metadata unavailable" MessageSeverity.error Option.none) cfg.name
``(Doc.Block.other (Block.errorExplanationHeader $(quote metadata)) #[])
| .some explan =>
Expand Down