Skip to content

Shorthand notation for erased arguments #98

@raffopazzo

Description

@raffopazzo

Introducing all function arguments required by later dependent-types can get verbose.

func choose(
  0 u64_t n,
  0 scope_t a,
  0 typename t,
    bool_t which,
    ref_t(array_t(t, n), a) p,
    ref_t(array_t(t, n), a) q
) -> ref_t(array_t(t, n), a);

It might be handy to have a shorthand notation to introduce erased arguments, something like this.

func choose(bool_t which, ref_t(array_t(@t, @n), @a) p, ref_t(array_t(t, n), a) q) -> ref_t(array_t(t, n), a);

This will require clarifying the rules of where each @x goes in the desugared argument list and in which order they are processed.

Metadata

Metadata

Assignees

No one assigned

    Labels

    featureNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions