This is a private forum.
Hello and welcome to discussion board of Software Foundations! Writing Coq code is enjoyable, but
some of
the exercises are really hard. Here, we can discuss these problems.
Attention: You shouldn't copy these solutions directly!
Use them as a hint in case you get stuck. If you have questions about these solutions, or if you have a
better one, feel free to leave a comment.
您好，欢迎来到《软件基础》的讨论板！书写 Coq 的代码给了我们极致丝滑的体验，但是有的题想了一天也毫无头绪。这里将是一个讨论这些问题的平台！
注意：您不能直接抄写这些答案！
在你遇到困难的时候，可以把他们作为一个提示。如果你对解法有任何的问题，或是你有更好的解法，欢迎在评论区留言。
If you are the teacher of a relevant course and would like me to close this discussion board,
please contact me (vbcpascal@outlook.com). I will privatize it unconditionally.
Authors of Software Foundations:
Organized by @vbcpascal.
Book: Version 5.8 (2020-09-09 20:57, Coq 8.12)
Solutions: Version 0.4 (2021-3-28 4:50, Coq 8.13, Coqdoc 8.11)