Int literals in ghost code

[arnaudgolfouse]

There should be an easy way to create an Int in ghost code. Currently you can do

ghost! {
    let x: Int = *Int::new(42);
};

But this is very inelegant.

[arnaudgolfouse]

One easy way would be to have int prefix, and in the ghost! macro desugars 42int into *Int::new(42). Its a bit weird since this suffix does not exists in pearlite though.

[jhjourdan]

That's only a solution to half the problem, since this will not work in ghost functions that do not use the ghost! macro.

What about *42.into(), by defining e.g., Ghost<Int> : From<u32>?

[arnaudgolfouse]

Unfortunately this struggles with type inference, even

ghost! {
    let x: Int = *0u32.into();
};

does not work 😕 (type annotations needed on the into call)

[jhjourdan]

@xldenis where is the Rust RFC with support for custom integer types?

[xldenis]

It never even made it to the stage of an rfc