709ea6cdf8
This default instance makes it possible to write things like `m!"the
constant is {.ofConstName n}"`.
Breaking change: This weakly causes terms to have a type of
`MessageData` if their type is otherwise unknown. For example:
* `m!"... {x} ..."` can cause `x` to have type `MessageData`, causing
the `let` definition of `x` to fail to elaborate. Fix: give `x` an
explicit type.
* Arithmetic expressions in `m!` strings may need a type ascription. For
example, if the type of `i` is unknown at the time the arithmetic
expression is elaborated, then `m!"... {i + 1} ..."` can fail saying
that it cannot find an `HAdd Nat Nat MessageData` instance. Two fixes:
either ensure that the type of `i` is known, or add a type ascription to
guide the `MessageData` coercion, like `m!"... {(i + 1 : Nat)} ..."`.
|
||
|---|---|---|
| .. | ||
| BuiltinSimprocs | ||
| Attr.lean | ||
| BuiltinSimprocs.lean | ||
| Diagnostics.lean | ||
| Main.lean | ||
| RegisterCommand.lean | ||
| Rewrite.lean | ||
| SimpAll.lean | ||
| SimpCongrTheorems.lean | ||
| Simproc.lean | ||
| SimpTheorems.lean | ||
| Types.lean | ||