Cannot find definitions of List, Cons and Nil

[Arrow7000]

I'm trying to run the code samples from the readme but can't because apparently Kind can't find the definitions of the List type and Cons and Nil constructors.

My code

// Applies a function to every element of a list
Map <a> <b> (list: List a) (f: a -> b) : List b
Map a b Nil              f             = Nil
Map a b (Cons head tail) f             = Cons (f head) (Map tail f)

// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
BlackFridayTheorem (n: Nat)     : Equal Nat (Nat.half (Nat.double n)) n
BlackFridayTheorem Nat.zero     = Equal.refl
BlackFridayTheorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (BlackFridayTheorem n)

But when I try to run it with kind2 run file.kind2 it gives me compile errors

   CHECKING  The file 'test.kind2'
   ERROR  Cannot find the definition 'List'.

      ┌──[test.kind2:2:20]
      │
    1 │    // Applies a function to every element of a list
    2 │    Map <a> <b> (list: List a) (f: a -> b) : List b
      │                       ┬───                  ┬───
      │                       │                     └Here!
      │                       └Here!
    3 │    Map a b Nil              f             = Nil

      Hint: Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md

   ERROR  Cannot find the definition 'Cons'.

      ┌──[test.kind2:4:10]
      │
    3 │    Map a b Nil              f             = Nil
    4 │    Map a b (Cons head tail) f             = Cons (f head) (Map tail f)
      │             ┬───                            ┬───
      │             │                               └Here!
      │             └Here!

      Hint: Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md

   ERROR  Cannot find the definition 'Nil'.

      ┌──[test.kind2:3:9]
      │
    2 │    Map <a> <b> (list: List a) (f: a -> b) : List b
    3 │    Map a b Nil              f             = Nil
      │            ┬──                              ┬──
      │            │                                └Here!
      │            └Here!
    4 │    Map a b (Cons head tail) f             = Cons (f head) (Map tail f)

      Hint: Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md

     FAILED  Took 0s

There is also no content in the file at the URL it suggests https://github.com/Kindelia/Kind2/blob/master/guide/naming.md

[algebraic-dev]

Kind does not have a prelude as the other languages like Haskell or Rust. So we recommend you to clone the Wikind repository that contains a lot of the common definitions that you would use and code inside it by now (as we don't have a build system :/)

[Arrow7000]

Ah gotcha. Do I need to copy and paste or import the code from the other files, or is it sufficient that my code is in the same directory as the other files?

[algebraic-dev]

You just have to code in the same directory.

[kings177]

closing this as the old kind2 has been archived at Kind2-old