|
73 | 73 | true |
74 | 74 | true |
75 | 75 | [Compiler.IR] [result] |
76 | | - def _private.lean.sint_basic.0.myId8 (x_1 : u8) : u8 := |
| 76 | + def _private.lean.sint_basic.0.myId8 (x_1 : i8) : i8 := |
77 | 77 | ret x_1 |
78 | | - def _private.lean.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged := |
79 | | - let x_2 : u8 := unbox x_1; |
80 | | - let x_3 : u8 := _private.lean.sint_basic.0.myId8 x_2; |
| 78 | + def _private.lean.sint_basic.0.myId8._boxed (x_1 : tobj) : tobj := |
| 79 | + let x_2 : i8 := unbox x_1; |
| 80 | + dec x_1; |
| 81 | + let x_3 : i8 := _private.lean.sint_basic.0.myId8 x_2; |
81 | 82 | let x_4 : tobj := box x_3; |
82 | 83 | ret x_4 |
83 | 84 | Int16 : Type |
@@ -155,11 +156,12 @@ true |
155 | 156 | true |
156 | 157 | true |
157 | 158 | [Compiler.IR] [result] |
158 | | - def _private.lean.sint_basic.0.myId16 (x_1 : u16) : u16 := |
| 159 | + def _private.lean.sint_basic.0.myId16 (x_1 : i16) : i16 := |
159 | 160 | ret x_1 |
160 | | - def _private.lean.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged := |
161 | | - let x_2 : u16 := unbox x_1; |
162 | | - let x_3 : u16 := _private.lean.sint_basic.0.myId16 x_2; |
| 161 | + def _private.lean.sint_basic.0.myId16._boxed (x_1 : tobj) : tobj := |
| 162 | + let x_2 : i16 := unbox x_1; |
| 163 | + dec x_1; |
| 164 | + let x_3 : i16 := _private.lean.sint_basic.0.myId16 x_2; |
163 | 165 | let x_4 : tobj := box x_3; |
164 | 166 | ret x_4 |
165 | 167 | Int32 : Type |
@@ -237,12 +239,12 @@ true |
237 | 239 | true |
238 | 240 | true |
239 | 241 | [Compiler.IR] [result] |
240 | | - def _private.lean.sint_basic.0.myId32 (x_1 : u32) : u32 := |
| 242 | + def _private.lean.sint_basic.0.myId32 (x_1 : i32) : i32 := |
241 | 243 | ret x_1 |
242 | 244 | def _private.lean.sint_basic.0.myId32._boxed (x_1 : tobj) : tobj := |
243 | | - let x_2 : u32 := unbox x_1; |
| 245 | + let x_2 : i32 := unbox x_1; |
244 | 246 | dec x_1; |
245 | | - let x_3 : u32 := _private.lean.sint_basic.0.myId32 x_2; |
| 247 | + let x_3 : i32 := _private.lean.sint_basic.0.myId32 x_2; |
246 | 248 | let x_4 : tobj := box x_3; |
247 | 249 | ret x_4 |
248 | 250 | Int64 : Type |
@@ -320,12 +322,12 @@ true |
320 | 322 | true |
321 | 323 | true |
322 | 324 | [Compiler.IR] [result] |
323 | | - def _private.lean.sint_basic.0.myId64 (x_1 : u64) : u64 := |
| 325 | + def _private.lean.sint_basic.0.myId64 (x_1 : i64) : i64 := |
324 | 326 | ret x_1 |
325 | 327 | def _private.lean.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj := |
326 | | - let x_2 : u64 := unbox x_1; |
| 328 | + let x_2 : i64 := unbox x_1; |
327 | 329 | dec x_1; |
328 | | - let x_3 : u64 := _private.lean.sint_basic.0.myId64 x_2; |
| 330 | + let x_3 : i64 := _private.lean.sint_basic.0.myId64 x_2; |
329 | 331 | let x_4 : tobj := box x_3; |
330 | 332 | ret x_4 |
331 | 333 | ISize : Type |
@@ -403,11 +405,11 @@ true |
403 | 405 | true |
404 | 406 | true |
405 | 407 | [Compiler.IR] [result] |
406 | | - def _private.lean.sint_basic.0.myIdSize (x_1 : usize) : usize := |
| 408 | + def _private.lean.sint_basic.0.myIdSize (x_1 : isize) : isize := |
407 | 409 | ret x_1 |
408 | 410 | def _private.lean.sint_basic.0.myIdSize._boxed (x_1 : tobj) : tobj := |
409 | | - let x_2 : usize := unbox x_1; |
| 411 | + let x_2 : isize := unbox x_1; |
410 | 412 | dec x_1; |
411 | | - let x_3 : usize := _private.lean.sint_basic.0.myIdSize x_2; |
| 413 | + let x_3 : isize := _private.lean.sint_basic.0.myIdSize x_2; |
412 | 414 | let x_4 : tobj := box x_3; |
413 | 415 | ret x_4 |
0 commit comments