Skip to content

Commit

Permalink
docs: eliminate mention of "function method" from "Getting Started" g…
Browse files Browse the repository at this point in the history
…uide (#5944)

Dafny functions (since Dafny 4.0 or so) are by default what previously
was called "function method". The previous default can be achieved with
ghost functions. In
#5006 (comment) it
was decided to not distract learners with that distinction already in
the "Getting Started" guide and to only introduce them to non-ghost
functions there.

This change eliminates a mention of "function method" that was probably
overlooked back then.

### Description
- Docs-only change. (Thus user-visible, but only in the documentation.)
- Inconsistency present also in the latest release, thus this change
should be backported to that.

- Tested by running `nix run nixpkgs#jekyll -- server --future` and then
navigating to `http://127.0.0.1:4000/docs/OnlineTutorial/guide` and
looking at the "Here we use `nats` […]" paragraph.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
das-g authored Nov 29, 2024
1 parent 1c2cf07 commit 1c5ebc1
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions docs/OnlineTutorial/guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -733,9 +733,8 @@ function fib(n: nat): nat

Here we use `nat`s, the type of
natural numbers (non-negative integers), which is often more convenient than
annotating everything to be non-negative. It turns out that we could make this
function a function method if we wanted to. But this would be extremely slow,
as this version of calculating the Fibonacci numbers has exponential
annotating everything to be non-negative. Using this function for actually calculating
the Fibonacci numbers would be extremely slow, as this implementation has exponential
complexity. There are much better ways to calculate the Fibonacci function. But
this function is still useful, as we can have Dafny prove that a fast version
really matches the mathematical definition. We can get the best of both worlds:
Expand Down

0 comments on commit 1c5ebc1

Please sign in to comment.