chore: more extensive LspEncoding test

This commit is contained in:
Wojciech Nawrocki 2021-07-21 20:27:17 -07:00 committed by Sebastian Ullrich
parent cfb5d34dd3
commit ef34cfd513

View file

@ -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