README

Author: yforster

README.md

@@ -9,6 +9,7 @@
   - Fabian Kunze
   - Nils Lauermann
   - Niklas Mück
+  - Haoyi Zeng
 - Maintainer:
   - Yannick Forster ([**@yforster**](https://github.com/yfrster))
 - License: [MIT License](LICENSE)
@@ -39,14 +40,15 @@ This library contains results on synthetic computability theory.
 - A proof of Post's theorem (`PT`) in `TuringReducibility/SemiDec.v`
 - A proof of Post's theorem about the arithmetical hierarchy in `PostsTheorem/PostsTheorem.v`
 - A proof of the Kleene-Post theorem in `PostsTheorem/KleenePostTheorem.v`
+- A solution to Post's problem in `PostsProblem`
 
 ## Installation
 
 ```sh
 opam switch create coq-synthetic-computability --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.17.0 coq-equations.1.3+8.17 coq-stdpp.1.8.0
+opam install coq.8.17.0 coq-equations.1.3+8.17 coq-metacoq-template.1.2+8.17 coq-stdpp.1.8.0
 cd theories
 make
 make install