From 3ea9edbd135ea9c5d8a14574d911d36805f355c5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 May 2020 16:06:57 -0700
Subject: [PATCH] chore: test for simulating old `{ Prod . ... }` syntax

---
 tests/lean/run/struct_inst_typed.lean | 2 ++
 1 file changed, 2 insertions(+)

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 _ _ }