-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Documentation of nameonly and default values for formals #3903
Changes from 1 commit
87ef620
2f633cc
13a17d8
5127a5c
e9859e9
83ca44a
f61f9f5
3e0e351
68de8fd
35badc7
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
- Loading branch information
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -4504,30 +4504,34 @@ as opposed to _required_. All required parameters must be declared | |
before any optional parameters. | ||
|
||
For example, | ||
``` | ||
<!-- %check-resolve %save f.tmp --> | ||
```dafny | ||
function f(x: int, y: int := 10): int | ||
``` | ||
may be called as either | ||
``` | ||
var i := f(1,2); | ||
var j := f(1); | ||
<!-- %check-resolve %use f.tmp --> | ||
```dafny | ||
const i := f(1,2); | ||
const j := f(1); | ||
``` | ||
where `f(1)` is equivalent to `f(1,10)` in this case. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add space after There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. OK |
||
|
||
Formal parameters may also be declared `nameonly`, in which case a call site | ||
must explicitly name the formal when providing its actual argument. | ||
|
||
The above function may be called as | ||
``` | ||
<!-- %no-check --> | ||
```dafny | ||
var k := f(y:=10, x:=2); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add a space on both sides of There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done |
||
``` | ||
using names; here, though there are no `nameonly` parameters so the names may be used | ||
or the actual arguments may be given in order. | ||
|
||
If a function is declared with a `nameonly` formal, then that formal's value must be given with a named assignment. | ||
For example, a function `ff` declared as | ||
``` | ||
function ff(x: int, nameonly y: int) | ||
<!-- %check-resolve --> | ||
```dafny | ||
function ff(x: int, nameonly y: int): int | ||
``` | ||
may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. "only" here feels a bit confusing. For one, the parameters don't have to be passed in as There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Right. Fixed. |
||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add space after
,
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK