diff options
| author | Thomas Letan <lthms@soap.coffee> | 2022-08-13 22:49:51 +0200 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2022-08-13 22:49:51 +0200 |
| commit | 28f27cb254a8073b573ffb43471a3b2b33bbef63 (patch) | |
| tree | b8d5536f16b734abe11a115bc4054dd95de44727 /site/posts | |
| parent | Hide cleapatra series for now (diff) | |
Fix two types reported by Wojciech Karpiel
Diffstat (limited to 'site/posts')
| -rw-r--r-- | site/posts/StronglySpecifiedFunctionsProgram.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v index c5763ea..94397cf 100644 --- a/site/posts/StronglySpecifiedFunctionsProgram.v +++ b/site/posts/StronglySpecifiedFunctionsProgram.v @@ -130,7 +130,7 @@ Qed. (** I want to highlight several things here: - - We return [x] (of type [a]) rather than a gigma-type, then <<Program>> is smart + - We return [x] (of type [a]) rather than a sigma-type, then <<Program>> is smart enough to wrap it. To do so, it tries to prove the post condition and because it fails, we have to do it ourselves (this is the Obligation we solve after the function definition.) @@ -169,7 +169,7 @@ Arguments vnil {a}. (** I had three functions in mind: [take], [drop] and [extract]. I learned few lessons. My main take-away remains: do not use - gigma-types, <<Program>> and dependent-types together. From my + sigma-types, <<Program>> and dependent-types together. From my point of view, Coq is not yet ready for this. Maybe it is possible to make those three work together, but I have to admit I did not find out how. As a consequence, my preconditions are defined as |