Clément Blaudeau

proof-lib/lean Turn the prelude into a proper Lean package

1

Currently, the Lean prelude lives inside the `proof-lib/lean` folder. To make it easier for users, it should be turned into a proper lean package

Rust understands integer literals as `i32` even in the middle of other integers computations : ```rust fn test (x:u64) -> u64 { x >> 3 } ``` [Open this code...

Even-though proving anything about Floats is very hard, we should print them. (from Lean's zulip : [#Program verification > We can’t prove anything about Float right?](https://leanprover.zulipchat.com/#narrow/channel/236449-Program-verification/topic/We.20can.E2.80.99t.20prove.20anything.20about.20Float.20right.3F/with/541702395))

Currently, the Lean backend relies on Lean typeclass resolution. It should be able to print explicit instances when necessary.

Rust supports [const generics](https://practice.course.rs/generics-traits/const-generics.html), which should be easy to add to the Lean Backend.

The solution should be inspired from the parent issue's discussion for the `F*` solution

The lean backend should support default implementations in trait definitions (and structures)

```rust fn test () { let x = (1,2).0; } ``` [Open this code snippet in the playground](https://hax-playground.cryspen.com/#lean/latest-main/gist=dfea5312daa0eaca8cbaf5e6075ea626) The projection is not rendered as it should : ```lean (Rust_primitives.Hax.Tuple0.Tuple0 (Rust_primitives.Hax.Tuple2.mk...

Right now the Lean backend looks at the `is_struct` and `is_record` flags on type definitions, and relies on implicit invariants (struct definitions have a single variant). It would be cleaner...