juvix/DuplicateInductiveParameterName.juvix at c5d8641142ea9dddfe75b0715a20d694b8bd8445 - juvix - gitea: Gitea Service

anoma/juvix

mirror of https://github.com/anoma/juvix.git synced 2024-12-01 00:04:58 +03:00

Jan Mas Rovira 2d666fd82c

Named arguments (#2250 )

- closes #1991 

This pr implements named arguments as described in #1991. It does not
yet implement optional arguments, which should be added in a later pr as
they are not required for record syntax.

# Syntax Overview

Named arguments are a convenient mehcanism to provide arguments, where
we give the arguments by name instead of by position. Anything with a
type signature can have named arguments, i.e. functions, types,
constructors and axioms.

For instance, if we have (note that named arguments can also appear on
the rhs of the `:`):
```
fun : {A B : Type} (f : A -> B) : (x : A) -> B := ... ;
```
With the traditional positional application, we would write
```
fun suc zero
```
With named arguments we can write the following:
1. `fun (f := suc) (x := zero)`.
2. We can change the order: `fun (x := zero) (f := suc)`.
3. We can group the arguments: `fun (x := zero; f := suc)`.
4. We can partially apply functions with named arguments: `fun (f :=
suc) zero`.
5. We can provide implicit arguments analogously (with braces): `fun {A
:= Nat; B := Nat} (f := suc; x := zero)`.
6. We can skip implicit arguments: `fun {B := Nat} (f := suc; x :=
zero)`.

What we cannot do:
1. Skip explicit arguments. E.g. `fun (x := zero)`.
2. Mix explicit and implicit arguments in the same group. E.g. `fun (A
:= Nat; f := suc)`
3. Provide explicit and implicit arguments in different order. E.g. `fun
(f := suc; x := zero) {A := Nat}`.

2023-07-18 10:32:34 +01:00

6 lines

103 B

Plaintext

Raw Blame History

 module DuplicateInductiveParameterName;
 type T (A : Type) (B : Type) (A : Type) := c : T A B A;
 end;