diff options
Diffstat (limited to 'site/posts/AlgebraicDatatypes.v')
| -rw-r--r-- | site/posts/AlgebraicDatatypes.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v index 1b24520..f32551c 100644 --- a/site/posts/AlgebraicDatatypes.v +++ b/site/posts/AlgebraicDatatypes.v @@ -1,3 +1,7 @@ +(** #<nav><p class="series">../coq.html</p> + <p class="series-prev">./ClightIntroduction.html</p> + <p class="series-next">./Coqffi.html</p></nav># *) + (** * Proving Algebraic Datatypes are “Algebraic” *) (** Several programming languages allow programmers to define (potentially @@ -93,7 +97,7 @@ Inductive prod (A B : Type) : Type := | pair : A -> B -> prod A B >> - #<div id="generate-toc"></div># + #<nav id="generate-toc"></nav># #<div id="history">site/posts/AlgebraicDatatypes.v</div># *) |