From 85c7772f4c499d22f5aa8707d5245c5dd8f61cbb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 26 Mar 2022 22:48:38 +0100 Subject: [PATCH] doc: fix ReST markup --- doc/examples/interp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/examples/interp.lean b/doc/examples/interp.lean index f32e8ed4c8..bf99e4a1d0 100644 --- a/doc/examples/interp.lean +++ b/doc/examples/interp.lean @@ -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