max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add test

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-07-20 21:30:27 -07:00 • committed by Sebastian Ullrich
parent 3accff6f48
commit 9664fc88e0
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
tests/lean/run/derivingLspEncoding.lean Normal file
View file

@ -0,0 +1,11 @@
import Lean.Server.FileWorker.LspEncoding
open Lean Server
structure Foo where
a : Array Nat
deriving LspEncoding with { withRef := true }
structure Bar where
fooRef : WithRpcRef Foo
deriving LspEncoding