We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0cef4e5 commit 82d457fCopy full SHA for 82d457f
ProofWidgets/Component/OfRpcMethod.lean
@@ -63,7 +63,7 @@ def MyComponent.rpc (ps : MyProps) : RequestM (RequestTask Html) :=
63
```
64
-/
65
elab "mk_rpc_widget%" fn:term : term <= expectedType => do
66
- let α ← mkFreshExprMVar (some (.sort levelOne)) (userName := `α)
+ let α ← mkFreshExprMVar (some (.sort .one)) (userName := `α)
67
let compT ← mkAppM ``Component #[α]
68
if !(← isDefEq expectedType compT) then
69
throwError "expected type{indentD expectedType}\nis not of the form{indentD compT}"
0 commit comments