1d8cf38ff9
Implements the pretty printer option `pp.numericTypes` for including a type ascription for numeric literals. For example, `(2 : Nat)`, `(-2 : Int)`, and `(-2 / 3 : Rat)`. This is useful for debugging how arithmetic expressions have elaborated or have been otherwise transformed. For example, with exponentiation is is helpful knowing whether it is `x ^ (2 : Nat)` or `x ^ (2 : Real)`. This is like the Lean 3 option `pp.numeralTypes` but it has a wider notion of a numeric literal. Also implements the pretty printer option `pp.natLit` for including the `nat_lit` prefix for raw natural number literals. Closes #3021 |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||