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.
Mhm... That's confusing. I've ran into the same issue with other Kata that use random tests. Is there something that I've done wrong?
Nim tests are broken, as some things have been deprecated.
Alright I see. I've yanked the kata at the moment, since this question is from somewhere else, and I might need to get their permission before publishing it.
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
I think it is, if we define a function in Preloaded that means that if
data.nat.pairing
is imported then Lean will complain about name collisions. So sayin Preloaded, and then in the Test only import
Solution
and notPreloaded
, then check the behaviour ofmkpair
to check that it is the one fromPreloaded
and notdata.nat.pairing
. I think this means that one way or another, the user cannot usemkpair
orunpair
fromdata.nat.pairing
.I'm not saying that this is a good idea though!
I suppose it is possible to make it so that people can't use
data.nat.pairing
, but as imports are transitive in lean, that also means that people can't use anything that importsdata.nat.pairing
.Lambda :
\Gl
, Forall :\all
, Exists :\ex
. If you press the backslash you should get a list of all the symbols that can be entered.There are pure ascii equivalents to some of theses (the basic katas can definitely be done in 100% ASCII), but in general it is preferred to use the symbols.
Coming up with names are hard :( Suggestions are welcome for the name.
There is a second part to the question, but as my solution already almost times out for the first part, I didn't add that in.
Questions:
mutual inductive
, but I can't seem to get it to behave the way that I want it to. Would that be preferable? In the context of this Kata I don't think there is any benefit to the TPIL version.Should maybe one of the first ones, say
even_plus_one_is_odd
be provided as an example with solution?Are the
even_[operation]_odd
andodd_[operation]_even
ones both needed? It's very easy to go from one to the other.Hello,
I've written a Lean version of this. Please take a look at it if you can :)
Loading more items...