chore: test for simulating old { Prod . ... } syntax

2020-05-20 16:06:57 -07:00 · 2020-05-20 16:06:57 -07:00 · 3ea9edbd13
commit 3ea9edbd13
parent 618d113075
1 changed files with 2 additions and 0 deletions
--- 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 _ _ }