// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //< https://doc.rust-lang.org/std/convert/enum.Infallible.html (empty enum) #[derive(Debug)] pub enum MyInfallible {} fn foo() -> Result<i64, MyInfallible> { Ok(1) } #[kani::proof] fn main() { let v = foo().unwrap(); assert!(v == 1); }