Kind1
Kind1 copied to clipboard
HigherOrderCO
Cannot find definitions of List, Cons and Nil
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
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 :/)
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?
