From 7930c2340bc27521f77bbb7039e3c4ccacc0ba51 Mon Sep 17 00:00:00 2001 From: RomanJos <42180076+RomanJos@users.noreply.github.com> Date: Sun, 31 Aug 2025 11:55:53 +0200 Subject: [PATCH 1/5] Update Polymorphism.lean --- book/FPLean/GettingToKnow/Polymorphism.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index b55dd83..617ce5b 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -444,11 +444,9 @@ context: :::paragraph This is because Lean was unable to fully determine the expression's type. -In particular, it could neither find the implicit type argument to {anchorName fragments}`List.head?`, nor the implicit type argument to {anchorName fragments}`List.nil`. -In Lean's output, {lit}`?m.XYZ` represents a part of a program that could not be inferred. -These unknown parts are called _metavariables_, and they occur in some error messages. -In order to evaluate an expression, Lean needs to be able to find its type, and the type was unavailable because the empty list does not have any entries from which the type can be found. -Explicitly providing a type allows Lean to proceed: +In particular, it could neither infer the implicit type argument to {anchorName fragments}`List.head?`, nor {anchorName fragments}`List.nil`. +In order to evaluate an expression, Lean must know its type. Here, the type is unavailable because the empty list does not contain any entries from which the type can be inferred. +Explicitly providing a type to the function {anchorName fragments}`List.head?` allows Lean to proceed: ```anchor headNone #eval [].head? (α := Int) @@ -458,7 +456,7 @@ Explicitly providing a type allows Lean to proceed: none ``` -The type can also be provided with a type annotation: +The type can also be provided with a type annotation for the value {anchorName fragments}`List.nil`: ```anchor headNoneTwo #eval ([] : List Int).head? @@ -469,7 +467,9 @@ none ``` The error messages provide a useful clue. -Both messages use the _same_ metavariable to describe the missing implicit argument, which means that Lean has determined that the two missing pieces will share a solution, even though it was unable to determine the actual value of the solution. +{lit}`?m.XYZ` are _metavariables_, Lean creates them as placeholder for missing values until they can be resolved. +Both error messages refer to the _same_ metavariable for the missing implicit argument, which means that once you specify the type for either {anchorName fragments}`List.head?` or {anchorName fragments}`List.nil` the other is resolved automatically. +Seeing the _same_ metavariable in multiple places is a sign that those unknowns share a single solution, and it often points to where extra type information needs to be supplied. ::: From 0f4a3a327d6ed031ff05dab87987225d97ff43f1 Mon Sep 17 00:00:00 2001 From: RomanJos <42180076+RomanJos@users.noreply.github.com> Date: Sun, 31 Aug 2025 14:03:19 +0200 Subject: [PATCH 2/5] Add @ notation --- book/FPLean/GettingToKnow/Polymorphism.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index 617ce5b..ae826fe 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -471,6 +471,22 @@ The error messages provide a useful clue. Both error messages refer to the _same_ metavariable for the missing implicit argument, which means that once you specify the type for either {anchorName fragments}`List.head?` or {anchorName fragments}`List.nil` the other is resolved automatically. Seeing the _same_ metavariable in multiple places is a sign that those unknowns share a single solution, and it often points to where extra type information needs to be supplied. +{lit}`@` is a notation used to make implicit argument explicit, which lean use to print the error message with arguments that could remain hidden from the developer : + +```anchor headHuhAt +#check @List.headd? Nat [4] +``` +```anchor headHuhAt +[4].headd? : Option Nat +``` +Is equivalent to : +```anchor headHuhAtTwo +#check List.headd? [4] +``` +```anchor headHuhAtTwo +[4].headd? : Option Nat +``` + ::: ## {lit}`Prod` From 88b87467ece685d111153445cef1afa7ef8473df Mon Sep 17 00:00:00 2001 From: RomanJos <42180076+RomanJos@users.noreply.github.com> Date: Sun, 31 Aug 2025 14:19:05 +0200 Subject: [PATCH 3/5] Update Polymorphism.lean copy-pasted this https://leanprover-community.github.io/archive/stream/113489-new-members/topic/namespace.20conflict.20advice.html --- book/FPLean/GettingToKnow/Polymorphism.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index ae826fe..0f06cff 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -471,7 +471,7 @@ The error messages provide a useful clue. Both error messages refer to the _same_ metavariable for the missing implicit argument, which means that once you specify the type for either {anchorName fragments}`List.head?` or {anchorName fragments}`List.nil` the other is resolved automatically. Seeing the _same_ metavariable in multiple places is a sign that those unknowns share a single solution, and it often points to where extra type information needs to be supplied. -{lit}`@` is a notation used to make implicit argument explicit, which lean use to print the error message with arguments that could remain hidden from the developer : +Moreover, {lit}`@` is a notation used to make implicit argument explicit, which lean use to print the error message with arguments that could remain hidden from the developer : ```anchor headHuhAt #check @List.headd? Nat [4] @@ -487,6 +487,11 @@ Is equivalent to : [4].headd? : Option Nat ``` +And, {lit}`_root_` is the top-level namespace, technically it's not a namespace and instead a prefix that the parser/elaborator specifically looks for when resolving names. +When a name starts with _root_, Lean looks for a declaration whose name is exactly what comes after _root_, ignoring aliases (names due to open or export). +When you're defining something, if the name doesn't start with _root_, it uses the current namespace as a prefix to get the name being defined, and if it does start with _root_ it just removes _root_ to get the name. +Namespaces will be introduced in the {ref "Can we refer to the Namespace paragraph directly here ?"}[next chapter] + ::: ## {lit}`Prod` From 05d435b3a769d11076593fb4cfd29749f6972e4e Mon Sep 17 00:00:00 2001 From: RomanJos <42180076+RomanJos@users.noreply.github.com> Date: Sun, 31 Aug 2025 14:21:22 +0200 Subject: [PATCH 4/5] Update Polymorphism.lean --- book/FPLean/GettingToKnow/Polymorphism.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index 0f06cff..a9f1304 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -474,20 +474,20 @@ Seeing the _same_ metavariable in multiple places is a sign that those unknowns Moreover, {lit}`@` is a notation used to make implicit argument explicit, which lean use to print the error message with arguments that could remain hidden from the developer : ```anchor headHuhAt -#check @List.headd? Nat [4] +#check @List.head? Nat [4] ``` ```anchor headHuhAt -[4].headd? : Option Nat +[4].head? : Option Nat ``` Is equivalent to : ```anchor headHuhAtTwo -#check List.headd? [4] +#check List.head? [4] ``` ```anchor headHuhAtTwo -[4].headd? : Option Nat +[4].head? : Option Nat ``` -And, {lit}`_root_` is the top-level namespace, technically it's not a namespace and instead a prefix that the parser/elaborator specifically looks for when resolving names. +And, {lit}`_root_` is the top-level, _root_, namespace, technically it's not a namespace and instead a prefix that the parser/elaborator specifically looks for when resolving names. When a name starts with _root_, Lean looks for a declaration whose name is exactly what comes after _root_, ignoring aliases (names due to open or export). When you're defining something, if the name doesn't start with _root_, it uses the current namespace as a prefix to get the name being defined, and if it does start with _root_ it just removes _root_ to get the name. Namespaces will be introduced in the {ref "Can we refer to the Namespace paragraph directly here ?"}[next chapter] From 6f154254621e579889f9ee9d51868211543265dd Mon Sep 17 00:00:00 2001 From: RomanJos <42180076+RomanJos@users.noreply.github.com> Date: Sun, 31 Aug 2025 16:30:53 +0200 Subject: [PATCH 5/5] Update Polymorphism.lean --- book/FPLean/GettingToKnow/Polymorphism.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/book/FPLean/GettingToKnow/Polymorphism.lean b/book/FPLean/GettingToKnow/Polymorphism.lean index a9f1304..b35852a 100644 --- a/book/FPLean/GettingToKnow/Polymorphism.lean +++ b/book/FPLean/GettingToKnow/Polymorphism.lean @@ -476,14 +476,14 @@ Moreover, {lit}`@` is a notation used to make implicit argument explicit, which ```anchor headHuhAt #check @List.head? Nat [4] ``` -```anchor headHuhAt +```anchorInfo headHuhAt [4].head? : Option Nat ``` Is equivalent to : ```anchor headHuhAtTwo #check List.head? [4] ``` -```anchor headHuhAtTwo +```anchorInfo headHuhAtTwo [4].head? : Option Nat ```