From ef34cfd5131de43b3ab862cacc72468cdda373c6 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Wed, 21 Jul 2021 20:27:17 -0700
Subject: [PATCH] chore: more extensive LspEncoding test

---
 tests/lean/run/derivingLspEncoding.lean | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/derivingLspEncoding.lean b/tests/lean/run/derivingLspEncoding.lean
index 741e430681..0ec8ff305b 100644
--- a/tests/lean/run/derivingLspEncoding.lean
+++ b/tests/lean/run/derivingLspEncoding.lean
@@ -2,10 +2,19 @@ import Lean.Server.FileWorker.LspEncoding
 
 open Lean Server
 
-structure Foo where
+structure FooRef where
   a : Array Nat
   deriving LspEncoding with { withRef := true }
 
+structure FooJson where
+  s : String
+  deriving FromJson, ToJson
+
 structure Bar where
-  fooRef : WithRpcRef Foo
+  fooRef : WithRpcRef FooRef
+  fooJson : FooJson
+  deriving LspEncoding
+
+structure BarTrans where
+  bar : Bar
   deriving LspEncoding