Function InteractiveCode

InteractiveCode(props: InteractiveCodeProps): Element
Displays a CodeWithInfos obtained via RPC from the Lean server.
Parameters
- props: InteractiveCodeProps
Returns Element
- Defined in lean4-infoview/src/infoview/interactiveCode.tsx:367