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

chore: rebase on 2022-07-10

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-07-10 21:43:53 -04:00 • committed by Leonardo de Moura
parent 625be05aa8
commit 0824e6b22b
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Widget/UserWidget.lean
View file

@ -7,6 +7,7 @@ Authors: E.W.Ayers
import Lean.Widget.Basic
import Lean.Data.Json
import Lean.Environment
import Lean.Elab.Eval
import Lean.Server
open Lean
@ -145,10 +146,8 @@ def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widg
syntax (name := widgetCmd) "#widget " ident term : command
private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := do
let e ← Term.elabTerm stx (mkConst ``Json)
let e ← Meta.instantiateMVars e
Term.evalExpr Json ``Json e
private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json := do
Term.evalTerm Json (mkConst ``Json) stx
@[implementedBy evalJsonUnsafe]
private opaque evalJson (stx : Syntax) : TermElabM Json