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/StronglySpecifiedFunctionsProgram.v | |
parent | Release of coqffi 1.0.0~beta4 (diff) |
2021 Spring redesign
Diffstat (limited to 'site/posts/StronglySpecifiedFunctionsProgram.v')
-rw-r--r-- | site/posts/StronglySpecifiedFunctionsProgram.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v index 1b4ab5f..c5763ea 100644 --- a/site/posts/StronglySpecifiedFunctionsProgram.v +++ b/site/posts/StronglySpecifiedFunctionsProgram.v @@ -5,7 +5,7 @@ to write strongly-specified functions in Coq. You can read the previous part #<a href="./StronglySpecifiedFunctionsRefine.html">here</a>#. # *) -(** #<div id="generate-toc"></div># +(** #<nav id="generate-toc"></nav># #<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *) @@ -341,7 +341,8 @@ Defined. (** val extract : 'a1 vector -> nat -> nat -> 'a1 vector **) let extract v e b = take (drop v b) (sub e b) ->> *) +>> + *) (** I was pretty happy, so I tried some more. Each time, using [nth], I managed to write a precise post condition and to prove it holds true. For instance, @@ -467,7 +468,8 @@ cannot be applied to the terms "b" : "Type" The 3rd term has type "Type" which should be coercible to "nat". ->> *) +>> + *) #[program] Fixpoint map2 {a b c n} @@ -520,4 +522,5 @@ cannot be applied to the terms "wildcard'" : "vector A n'" The 3rd term has type "vector A n'" which should be coercible to "nat". ->> *) +>> + *) |