Son HO

If I hide a `StackInline` function's implementation behind an interface and don't declare it `inline_for_extraction`, Kremlin generates code where the function is not inlined, while I would have expected it...

Do not use the `Result` type for functions which syntactically never fail

10

For now we always use the `Result` type in the output type of the functions we generate. This can make it cumbersome to prove theorems about simple functions. For instance,...

We should add the following test: ```rust fn foo() { while true { bar() } } ```

Today, when printing spans for external declarations we generated ugly strings, leading to noise in the generated code. For instance: ```lean /- [core::cell::{core::cell::Cell#10}::get]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26 Name pattern: core::cell::{core::cell::Cell}::get...

It can happen that the compilation generates warnings (for instance, clippy warnings): I want to make sure it doesn't happen (i.e., all warnings are addressed before we merge).

This is starting to be critical, in particular to explain the policy with regards to the test regeneration, and how to add definitions to the standard library of the different...

Use `omega` instead of `linarith` in the `scalar_tac` tactic

1

The `omega` tactic seems more performant than `linarith`, so it is worth at least experimenting. In particular, I wonder how good it is at reasoning about goals which contain both...

Names like `back_'a` are not very pretty: `back'a` would be better. Also, when calling a function, we sometimes name `back` a value (i.e., a backward function with no inputs), which...

This might prove useful: https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2024-03-28

If `x` is a machine integer (e.g., `U32`), Lean often displays `x` coerced to `Int` as `x.val` instead of `↑x`. This can make the proof states quite difficult to parse,...