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

fix: sorried errors in rpcServerMethod

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-05-22 14:43:32 -04:00 • committed by Leonardo de Moura
parent c2fdcad443
commit 4972f214be
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Server/Rpc/RequestHandling.lean
View file

@ -108,9 +108,10 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do
throwError s!"{errMsg}: already registered"
let wrappedName := method ++ `_rpc_wrapped
let procT := mkConst ``RpcProcedure
let proc ← MetaM.run' <| TermElabM.run' <| do
let c ← Lean.Elab.Term.elabTerm (← `(wrapRpcProcedure $(quote method) _ _ $(mkIdent method))) procT
return ← instantiateMVars c
let proc ← MetaM.run' <| TermElabM.run' <| withoutErrToSorry do
let stx ← ``(wrapRpcProcedure $(quote method) _ _ $(mkIdent method))
let c ← Lean.Elab.Term.elabTerm stx procT
instantiateMVars c
addAndCompile <| Declaration.defnDecl {
name := wrappedName
type := procT