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

doc: fix ReST markup

Browse source
This commit is contained in:
Sebastian Ullrich 2022-03-26 22:48:38 +01:00
parent bef34e30e7
commit 85c7772f4c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/examples/interp.lean
View file

@ -22,7 +22,7 @@ inductive Vector (α : Type u) : Nat → Type u
| cons : α → Vector α n → Vector α (n+1)
/-|
We can overload the `List.cons` notation `::` and use it to create `Vector`s.
We can overload the `List.cons` notation `::` and use it to create `Vector`\ s.
-/
infix:67 " :: " => Vector.cons