From 00bb8475af2a57118153708a9f069f94da643bad Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 16 Dec 2024 15:01:35 +0100 Subject: [PATCH] feat: improve description of instance implicits (#218) Closes #193 --- Manual/Terms.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Manual/Terms.lean b/Manual/Terms.lean index 2d211d8..c8091ba 100644 --- a/Manual/Terms.lean +++ b/Manual/Terms.lean @@ -382,7 +382,7 @@ The {keywordOf Lean.Parser.Term.fun}`=>` may be replaced by {keywordOf Lean.Pars Function abstractions may also use pattern matching syntax as part of their parameter specification, avoiding the need to introduce a local variable that is immediately destructured. This syntax is described in the {ref "pattern-fun"}[section on pattern matching]. -## Implicit Functions +## Implicit Parameters %%% tag := "implicit-functions" %%% @@ -407,7 +407,10 @@ Implicit parameters come in three varieties: : Instance implicit parameters Arguments for {deftech}_instance implicit_ parameters are found via {ref "instance-synth"}[type class synthesis]. - Instance implicit parameters are written in square brackets (`[` and `]`), and in most cases omit the parameter name because instances synthesized as parameters to functions are already available in the functions' bodies, even without being named explicitly. + Instance implicit parameters are written in square brackets (`[` and `]`). + Unlike the other kinds of implicit parameter, instance implicit parameters that are written without a `:` specify the parameter's type rather than providing a name. + Furthermore, only a single name is allowed. + Most instance implicit parameters omit the parameter name because instances synthesized as parameters to functions are already available in the functions' bodies, even without being named explicitly. ::::keepEnv :::example "Ordinary vs Strict Implicit Parameters"