What's the motivation behind this kata? I don't understand why we're proving equality of a bunch of proof terms.

I loved the simplicity of this kata. Very cool.

Should be fixed now, I've inserted the relevant calls to idtac "<PASSED::>" and idtac "<FAILED::>". I don't think it's necessary to open an issue there, as this is a rather esoteric kata with correspondingly esoteric methods of testing.

@JasonGross

I'm a bit confused why I need to use ...

The runner needs to know if the solution is a valid one somehow. And we decided what's considered valid in https://github.com/codewars/codewars-runner-cli/issues/425

I can add Print Assumptions I at the bottom just to conform to the way things are set up, but that seems silly, and https://github.com/codewars/coq_codewars isn't flexible enough to do the kind of check needed for this kata. Is there a way to get the right output for the test runner to accept things using idtac?

Can you open a new issue at https://github.com/codewars/coq_codewars ? We can discuss what can be done over there.

I'm a bit confused why I need to use Print Assumptions or https://github.com/codewars/coq_codewars ; if the test file runs to completion without throwing errors, then this should be considered succeeding. I can add Print Assumptions I at the bottom just to conform to the way things are set up, but that seems silly, and https://github.com/codewars/coq_codewars isn't flexible enough to do the kind of check needed for this kata. Is there a way to get the right output for the test runner to accept things using idtac?

Ah, I had assumed not being able to complete was obvious from my original comment so I didn't understand the point of your comment.

After trying to understand it, I thought your comment was referring to the fact I unpublished it (and making it impossible to submit a solution). My bad.

That's exactly what I just said...

? It's currently impossible to complete (it was actually never possible) because there's no test output. I don't think it should be kept published.

This kata probably got published because of the bug where publishing from a draft state bypasses the check.

(making it impossible to submit a solution)

@JasonGross

This kata doesn't seem to output anything for the runner to process.

The current output is:

(?a : A) : C true
    : C true
where
?a : [ |- A]
success!
I
    : True
fun a : Preloaded.A => a : Preloaded.C true
    : forall _ : Preloaded.A, Preloaded.C true

Please use https://github.com/codewars/coq_codewars or Print Assumptions.

I've unpublished the kata for now.

Yes, this is part of the semantics of Qed.

Thanks, I didn't know the behavior of Defined is different from Qed's. It works after I changed Qed to Defined.

BTW, if Qed is used to close the proofs, compute does nothing.

.

Okay, this time it worked, though I could have sworn I had done that last time.

You need to update that select box to 8.11, then click Validate Solution, and you'll see that you'll have to update the code to be compatible with 8.11.
I mean, the CW runner requires there to be tests or it thinks they failed, so you need to add a test.