diff --git a/tests/lean/run/ubscalar.lean b/tests/lean/run/ubscalar.lean new file mode 100644 index 0000000000..2a8640f6a8 --- /dev/null +++ b/tests/lean/run/ubscalar.lean @@ -0,0 +1,16 @@ +structure Foo := +(flag : Bool := false) +(x : UInt16 := 0) +(z : UInt32 := 0) +(w : UInt64 := 0) +(h : USize := 0) +(xs : List Nat := []) + +set_option trace.compiler.ir.init true + +def f (s : Foo) : Foo := +{ x := s.x + 1, .. s } + +def g (flag : Bool) : Foo := +let s : Foo := { x := 10, flag := flag }; +f s