diff options
Diffstat (limited to 'site/posts/StronglySpecifiedFunctions.org')
| -rw-r--r-- | site/posts/StronglySpecifiedFunctions.org | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org index 805b944..83148c6 100644 --- a/site/posts/StronglySpecifiedFunctions.org +++ b/site/posts/StronglySpecifiedFunctions.org @@ -1,8 +1,7 @@ -#+OPTIONS: toc:nil num:nil +#+TITLE: A Series on Strongly-Specified Functions in Coq -#+BEGIN_EXPORT html -<h1>A Series on Strongly-Specified Functions in Coq</h1> -#+END_EXPORT +#+SERIES: ../coq.html +#+SERIES_NEXT: ./Ltac.html Using dependent types and the ~Prop~ sort, it becomes possible to specify functions whose arguments and results are constrained by properties. Using such |