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