feat(lean): support for const parameters

[clementblaudeau]

This PR adds support for const parameters on functions and traits. They are represented as normal parameters.

/// Test def site
fn f<const N1: usize>(x : usize) -> usize {
    N1 + x + 1 
}

/// Test call site
fn test() -> usize { 
    f::<1>(1) 
    + f::<{ if true { 1 } else { 1 / 0 } }>(2)
}

--  Test def site
def Playground.f (N1 : usize) (x : usize) : RustM usize := do
  ((← (N1 +? x)) +? (1 : usize))

--  Test call site
def Playground.test (_ : Rust_primitives.Hax.Tuple0) : RustM usize := do
  ((← (Playground.f ((1 : usize)) (1 : usize)))
    +? (← (Playground.f ((1 : usize)) (2 : usize))))

Open this code snippet in the playground

This adds a necessary step towards the support of arrays with non integer-literal size (#1713). During the work on this PR, the issue #1796 was uncovered, which explains the 2 added negative tests.

[abentkamp]

As commented in #1796, issue #1796 could quite easily be fixed. But I think we can merge this PR first.