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

fix: image paths

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-08-06 15:59:57 -04:00 • committed by Sebastian Ullrich
parent 962a4bfa78
commit 7b7e2f54da
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/examples/widgets.lean
View file

@ -8,7 +8,7 @@ Proving and programming are inherently interactive tasks. Lots of mathematical o
structures are visual in nature. *User widgets* let you associate custom interactive UIs with
sections of a Lean document. User widgets are rendered in the Lean infoview.
![Rubik's cube](images/widgets_rubiks.png)
![Rubik's cube](../images/widgets_rubiks.png)
## Trying it out
@ -165,7 +165,7 @@ Finally we can try out the widget.
#widget checkWidget .null
/-!
![`#check` as a service](images/widgets_caas.png)
![`#check` as a service](../images/widgets_caas.png)
## Building widget sources