so far, our reference manual did not mention these at all, this takes
the discussion of recursive definition out of the “equation compiler”
section, put it into its own section, and expands it a bit.
This is more a MVP doc change to at least mention the features briefly,
and not the most polished and thought through didactic exposition. But
it provides a start for more improvements.
---------
Co-authored-by: Arthur Adjedj <arthur.adjedj@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This change
* moves `termination_by` and `decreasing_by` next to the function they
apply to
* simplify the syntax of `termination_by`
* apply the `decreasing_by` goal to all goals at once, for better
interactive use.
See the section in `RELEASES.md` for more details and migration advise.
This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
This PR fixes the documentation error in "Extended Setup Notes", where
the path of builded binary is pointed to
`./build/bin/foo`, but the truly path is `./lake/build/bin/foo`.
---
Closes#3094 (`RFC` or `bug` issue number fixed by this PR, if any)
Since the vscode-lean4 setup guide allows us to provide information on
setting up Lean 4 tailored to the user's operating system, this PR
adjusts the quickstart guide to reference the vscode-lean4 setup guide
instead.
This Github action automatically updates `stage0` on `master` if
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h`
are out of sync there.
It bypasses the merge queue to be quick, this way, an out-of-date stage0
on on
master should only exist for a few minutes.
Needs access to a _deploy SSH key_ with write permission.
Implements "gaps" in string literals. These are escape sequences of the
form `"\" newline whitespace+` that have the interpretation of an empty
string. For example,
```
"this is \
a string"
```
is equivalent to `"this is a string"`. These are modeled after string
continuations in
[Rust](https://doc.rust-lang.org/beta/reference/tokens.html#string-literals).
Implements RFC #2838
