Not sure about the naming yet. Alternative names: Context declarations, "with declarations".
Prior art: Idris 1.
A parameter declaration contains a list/spline of parameters and a list of data, value and other parameter declarations.
It allows the user to group parameters common to some selected declarations. They can probably be fully handled in the lowerer without touching the name resolver.
Helps writing code and perhaps also reading code, albeit not necessarily. In fact, the chance of worsened readability is the main distrust of mine in regards to this feature. Also, it's not flexible in respect to the order of parameters.
Introduces keyword with (…).
Example:
Surface language:
with '(A: Type) '(n: Nat) (v: Vector A n) of
reverse: Vector A n = ?reverse
length: Nat = n
compare ''(o: Ord A) '(m: Nat) (w: Vector A m): Ordering = ?compare
Lowered language:
reverse '(A: Type) '(n: Nat) (v: Vector A n): Vector A n = ?reverse
length '(A: Type) '(n: Nat) (v: Vector A n): Nat = n
;; note: heinous order of arguments!
compare '(A: Type) '(n: Nat) (v: Vector A n) ''(o: Ord A) '(m: Nat) (w: Vector A m): Ordering = ?compare
Not sure about the naming yet. Alternative names: Context declarations, "with declarations". Prior art: Idris 1.
A parameter declaration contains a list/spline of parameters and a list of data, value and other parameter declarations. It allows the user to group parameters common to some selected declarations. They can probably be fully handled in the lowerer without touching the name resolver.
Helps writing code and perhaps also reading code, albeit not necessarily. In fact, the chance of worsened readability is the main distrust of mine in regards to this feature. Also, it's not flexible in respect to the order of parameters.
Introduces keyword
with(…).Example:
Surface language:
Lowered language:
Personally generally not in favor.