You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
These might be a little less confusing to programmers from procedural languages, and might help us to simplify compilation to Rust somewhat (avoiding the need for an uncurring pass in the compiler). In practice, this would mean that we would use 'telescopes' for parameter lists rather than single parameter functions. For example:
Array : (len : {l : Int | l >= 0}, Elem : Type) -> Type
Array.get : [len, Elem](array : Array len Elem, index : {i : Int | i < len}) -> Elem
Array.repeat : [Elem](len : {l : Int | l >= 0}, elem : Elem) -> Array len Elem
Not sure about the syntax for implicit parameters. Square brackets might conflict with array terms.
The text was updated successfully, but these errors were encountered:
These might be a little less confusing to programmers from procedural languages, and might help us to simplify compilation to Rust somewhat (avoiding the need for an uncurring pass in the compiler). In practice, this would mean that we would use 'telescopes' for parameter lists rather than single parameter functions. For example:
Not sure about the syntax for implicit parameters. Square brackets might conflict with array terms.
The text was updated successfully, but these errors were encountered: