Manually added to the test suite
You're completely right. It's hopefully fixed now.
I don't think so?
Maybe the use of lemmas in Data.Nat.Properties sould be prohibited?
I fixed it in the editor. There was more wrong with it.
Approved! You're teaching me Coq man.
This comment is hidden because it contains spoiler information about the solution
Sincerely hope I didn't make any mistakes.
Thanks. Approved, but it might take a while to appear because the background job queue is really full right now :(
I'm really sorry to make these mistakes. Swapped code block back, added setup code, updated description.
They're displayed as "descriptions of 2 languages co-exists", but it's actually separated after publishing.