Ignore Lifetimes

[yannbolliger]

We assume that rustc has done a good job at borrow checking and lifetime inference before the extraction phase. Therefore it is safe to ignore/erase lifetimes when extraction Rust to Stainless.

The failure: Unsupported tree: Cannot extract generic parameter '_ of kind: Lifetime only happens when using methods on generic types containing references like Option<&T>.copied(). As these methods are not understood by Stainless at the moment anyway, the issue is of very low priority.

Example:

pub fn main() {
  let opt = Some(&123).copied();
  assert!(matches!(opt, Some(123)));
}