Loading collection data...
Collections are a way for you to organize kata so that you can create your own training routines. Every collection you create is public and automatically sharable with other warriors. After you have added a few kata to a collection you and others can train on the kata contained within the collection.
Get started now by creating a new collection.
Added imports to description
Displayed preloaded code is missing the import for
≢and∘.Unpublished because the existing similar kata has an Agda translation now.
I just could not see anything specific in the description, and I did not know if I am missing something, or maybe the "what" can be deduced or inferred from current description.
Anyway I see you added it to description.
Ah. I just meant "Prove collections of universal arrows equivalent to Adjoint functor". Maybe I should use more specific phrasing. : )
Actually, this kind of kata is always encouraged to first solve locally. So you can use various tools provided by your proof assistant to construct the proof. As the name "interactive theorem prover" suggested.
And because the only thing test case doing is verify the type is correct. Thence your proof isn't actually "running" anyways. Only the "compiler" is doing the jobs making sure your proof "compiles".
Therefor if your proof assistant accepted your proof locally. You can pretty sure your proof is correct and verified. Because the sample test case is exactly same as real test case.
I think rather we should greatly increase the global timeout limit for proof assistant related languages. Because in general the above applied to most of them.
Best regards <3
Which "one of them" exactly? Should it be stated explicitly somewhere in the description, or maybe it is and my TP-stupid ass cant see it?
But if proof times out, then is it possible to know it's correct? The "timeout check" is not a separate test. If tests time out, then a submitted solution is not completely verified, right?
Essentially a duplicate of the following kata.
Please unpublish this kata and translate the existing approved kata to Agda.
glad I didn't have to do that because my function is 100% correct :)
It's not about size. In point-free version
cycle "10"will most likely be evaluated only once (even if you don't really need it in this case)This comment is hidden because it contains spoiler information about the solution
Approved
Glad that I'm not the only one who hacked last test case around.
It really should have been a different kata because it made it one kyu harder than translations in other languages.
Lean Translation Kumited - please accept :-D
Loading more items...