From 10fe453cf62c0bfd5abda2dcda872489afc7f3e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Jul 2019 10:11:35 -0700 Subject: [PATCH] test(tests/lean/run/ubscalar): save UB scalar field test --- tests/lean/run/ubscalar.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/lean/run/ubscalar.lean 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