Ad
  • Custom User Avatar

    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?

  • Custom User Avatar

    Nim tests are broken, as some things have been deprecated.

    /workspace/solution_tests.nim(63, 7) template/generic instantiation of `suite` from here
    /workspace/solution_tests.nim(65, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
    /workspace/solution_tests.nim(63, 7) template/generic instantiation of `suite` from here
    /workspace/solution_tests.nim(66, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
    /workspace/solution_tests.nim(70, 7) template/generic instantiation of `suite` from here
    /workspace/solution_tests.nim(72, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
    /workspace/solution_tests.nim(70, 7) template/generic instantiation of `suite` from here
    /workspace/solution_tests.nim(73, 35) Warning: Deprecated since v0.18.0; use 'rand' instead; random is deprecated [Deprecated]
    Error: execution of an external program failed: '/workspace/tests '
    
  • Custom User Avatar

    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.

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    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 say

    namespace nat
    
    def mkpair (a b : ℕ) := a + b
    
    end nat
    

    in Preloaded, and then in the Test only import Solution and not Preloaded, then check the behaviour of mkpair to check that it is the one from Preloaded and not data.nat.pairing. I think this means that one way or another, the user cannot use mkpair or unpair from data.nat.pairing.

    I'm not saying that this is a good idea though!

  • Custom User Avatar

    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 imports data.nat.pairing.

  • Custom User Avatar

    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.

  • Custom User Avatar

    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.

  • Custom User Avatar

    Questions:

    1. TPIL uses a different definition of even and odd with 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.
    mutual inductive even, odd
    with even : ℕ → Prop
    | even_zero : even 0
    | even_succ : ∀ n, odd n → even (n + 1)
    with odd : ℕ → Prop
    | odd_succ : ∀ n, even n → odd (n + 1)
    
    1. Should maybe one of the first ones, say even_plus_one_is_odd be provided as an example with solution?

    2. Are the even_[operation]_odd and odd_[operation]_even ones both needed? It's very easy to go from one to the other.

  • Custom User Avatar

    Hello,

    I've written a Lean version of this. Please take a look at it if you can :)

  • Loading more items...