Parameters
Defining parameters
| Lean 4 | Scala 3 | |
|---|---|---|
| Single argument | (n: Int) |
(n: Int) |
| Multiple arguments groups, same type | (n m: Int) |
(n: Int) (m: Int) |
| Multiple arguments groups, different types | (n: Int) (s: String) |
(n: Int) (s: String) |
| Tupled arguments | (ns: Int × String) |
(n: Int, s: String) |
| Type arguments, required | (A: Type)(A) |
|
| Type arguments, inferrable | [A <: Any][A] |
|
| Type arguments, always inferred | {A: Type}{A} |
|
| type class arguments, named | [a: A] |
(using a: A) |
| type class arguments, anonymous | [A] |
(using A) |
Passing arguments to parameters
| Lean 4 | Lean 4 | Scala 3 | Scala 3 |
|---|---|---|---|
def f (n m: Int) |
f 1 2 |
def f(n: Int)(m: Int) |
f(1)(2) |
def f (ns: Int × Int) |
f (1, 2) |
def f(n: Int, m: Int) |
f(1, 2) |
def f (A: Type) (a: A) |
f Int 1f _ 1 |
||
def f[A] (a: A) |
f[Int](1)f(1) |
||
def f {A: Type} (a: A) |
f 1@f Int 1f (A := Int) 1 |
||
def f (n: Int) [A] |
f 1@f 1 af 1 (A := a) |
def f (n: Int) [A] |
f 1f 1 (using a) |
In Lean when an argument is defined using {A} it can’t be passed explicitly. To do so we need to use the @ modifier, which makes all argument explicit:
-- correct:
length ["a", "b"]
-- incorrect: `String` can't be passed explicitly
length String ["a", "b"]
-- fix, use the `@` modifier:
@length String ["a", "b"]