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