The following rust example:

fn test() -> bool {
    let x: Option<u8> = None;
    x.is_none()
}

gets translated to the following lean:

def test : Result Bool := do
  ok (core.option.Option.is_none none)

And here lean fails because it doesn't know how to instantiate the type argument for option of the none literal.