diff options
author | Thomas Letan <lthms@soap.coffee> | 2021-03-28 00:03:41 +0100 |
---|---|---|
committer | Thomas Letan <lthms@soap.coffee> | 2021-03-28 14:19:29 +0200 |
commit | 495f9db0606b0ed09e6fac59dc32de4cdc8c0087 (patch) | |
tree | 82ea5c5e247c664de247a0f3818f393ffdb00067 /site/posts/ClightIntroduction.v | |
parent | Release of coqffi 1.0.0~beta4 (diff) |
2021 Spring redesign
Diffstat (limited to 'site/posts/ClightIntroduction.v')
-rw-r--r-- | site/posts/ClightIntroduction.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v index 4bd9a52..85d084b 100644 --- a/site/posts/ClightIntroduction.v +++ b/site/posts/ClightIntroduction.v @@ -1,3 +1,7 @@ +(** #<nav><p class="series">../coq.html</p>
+ <p class="series-prev">./RewritingInCoq.html</p>
+ <p class="series-next">./AlgebraicDatatypes.html</p></nav># *)
+
(** * A Study of Clight and its Semantics *)
(* begin hide *)
From Coq Require Import List.
@@ -12,7 +16,7 @@ Import ListNotations. challenged myself to study Clight and its semantics. This write-up is the
result of this challenge, written as I was progressing.
- #<div id="generate-toc"></div>#
+ #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/ClightIntroduction.v</div># *)
|