1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-25 16:45:20 +03:00
juvix/include/package
Łukasz Czajka 2e38aa609f
Unify type signature declaration syntax (#3178)
* Closes #2990 
* Allows type signatures for constructors, record fields and axioms to
have the same form as in function definitions, e.g.,
```
field {A} {{M A}} (arg1 arg2 : A) : List A
```
* For constructors, this introduces an ambiguity between record and GADT
syntax with names. For example,
```
ctr {
  A : Type
}
```
can be confused by the parser with initial part of GADT type signature:
```
ctr {A : Type} : A -> C A
```
For now, this is resolved by preferring the record syntax. Hence, it's
currently not possible to use type signatures with implicit arguments
for constructors. Ultimately, the `@` in record syntax should be made
mandatory, which would resolve the ambiguity:
```
ctr@{
  A : Type
}
```

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2024-11-20 15:57:15 +00:00
..
PackageDescription Unify type signature declaration syntax (#3178) 2024-11-20 15:57:15 +00:00
Package.juvix Fix the global 'package' package so that modules within it can be type-checked independently (#2526) 2023-11-21 15:20:00 +00:00