diff --git a/tests/lean/run/struct_inst_typed.lean b/tests/lean/run/struct_inst_typed.lean index 3b464482ee..dcbd2d43c1 100644 --- a/tests/lean/run/struct_inst_typed.lean +++ b/tests/lean/run/struct_inst_typed.lean @@ -5,3 +5,5 @@ structure S := #check { x := 10, y := true, z := "hello" : S } + +#check { fst := "hello", snd := "world" : Prod _ _ }