diff options
| author | Thomas Letan <lthms@soap.coffee> | 2021-08-20 11:35:45 +0200 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2021-08-20 11:35:45 +0200 |
| commit | 3f657326c3b68eeea7f16aeaf06dc5ff8fdd61c4 (patch) | |
| tree | b3860f353a94bf2adbb508f38b0bd982cdef77df /site/posts/CoqffiEcho.org | |
| parent | Advertise the release of coqffi beta 6 and 7 (diff) | |
Fix a Coq warning
Diffstat (limited to 'site/posts/CoqffiEcho.org')
| -rw-r--r-- | site/posts/CoqffiEcho.org | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org index b9c531e..8d48c48 100644 --- a/site/posts/CoqffiEcho.org +++ b/site/posts/CoqffiEcho.org @@ -333,7 +333,7 @@ typeclass. #+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v Notation "'let_rec*' f x ':=' p 'in' q" := (let f := mfix (fun f x => p) in q) - (at level 61, x pattern, f ident, q at next level, right associativity). + (at level 61, x pattern, f name, q at next level, right associativity). #+END_SRC Note that ~mfix~ does /not/ check whether or not the defined function |