38d9a7c063
@Kha Could you please take a look at this repro? When I use the compiler, ``` ./run.sh usizeBug.lean ``` I get the expected answer: `2`. When I use the interpreter, ``` ../../bin/lean --run usizeBug.lean ``` I get `1`. I found the problem today, and managed to isolate the problem to this small repro.
9 lines
136 B
Text
9 lines
136 B
Text
structure S :=
|
|
(n : Nat)
|
|
(u : USize)
|
|
|
|
@[noinline] def f (u : USize) : S :=
|
|
{ n := 0, u := u }
|
|
|
|
def main : IO Unit :=
|
|
IO.println (f 2).u
|