| [result] | |
| def MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 (x_1 : @& obj) : u8 := | |
| case x_1 : obj of | |
| MyOption.none → | |
| let x_2 : u8 := 0; | |
| ret x_2 | |
| MyOption.some → | |
| let x_3 : u8 := 1; | |
| ret x_3 | |
| def isSomeWithInstanceNat (x_1 : @& obj) : u8 := | |
| let x_2 : usize := 0; | |
| let x_3 : obj := Array.uget ◾ x_1 x_2 ◾; | |
| let x_4 : u8 := MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 x_3; | |
| dec x_3; | |
| ret x_4 | |
| def MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1._boxed (x_1 : obj) : obj := | |
| let x_2 : u8 := MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 x_1; | |
| dec x_1; | |
| let x_3 : obj := box x_2; | |
| ret x_3 | |
| def isSomeWithInstanceNat._boxed (x_1 : obj) : obj := | |
| let x_2 : u8 := isSomeWithInstanceNat x_1; | |
| dec x_1; | |
| let x_3 : obj := box x_2; | |
| ret x_3 |