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

chore: hide weird RpcEncoding behind Nonempty

Browse source
This commit is contained in:
Gabriel Ebner 2022-07-17 21:08:16 +02:00 • committed by Sebastian Ullrich
parent ed5e0f098c
commit d36552848c
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Server/Rpc/Basic.lean
View file

@ -46,8 +46,8 @@ class RpcEncoding (α : Type) (β : outParam Type) where
rpcDecode {m : Type → Type} [Monad m] [MonadRpcSession m] : β → ExceptT String m α
export RpcEncoding (rpcEncode rpcDecode)
instance : Inhabited (RpcEncoding α β) where
default := { rpcEncode := fun _ => throw "unreachable", rpcDecode := fun _ => throw "unreachable" }
instance : Nonempty (RpcEncoding α β) :=
⟨{ rpcEncode := fun _ => throw "unreachable", rpcDecode := fun _ => throw "unreachable" }⟩
instance [FromJson α] [ToJson α] : RpcEncoding α α where
rpcEncode := pure

4
src/Lean/Server/Rpc/Deriving.lean
View file

@ -25,7 +25,9 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
rpcDecode := WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm)
@[implementedBy unsafeInst]
instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef := default
opaque inst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef
instance : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef := inst
)
elabCommand cmds
return true