Booleanos

Semelhantemente, podemos declarar o tipo Bool, para booleanos:

type Bool {
	true
	false
}

Nós estamos declarando nossos próprios booleanos só para demonstrar como fazer tudo do zero. O Kind tem a sua implementação padrão de booleanos no pacote padrão (o Wikind), junto de várias outras estruturas e provas. Na verdade, no momento de escrita, é necessário que você esteja trabalhando dentro da pasta Wikind para fazer provas e teoremas, pois ainda não temos um gerenciador de pacote e os utilitários de resolução de provas não são built-in.

Funções que funcionam sobre booleanos são definidas do mesmo jeito que visto anteriormente:

// Negação lógica
Notb (b: Bool) : Bool
Notb Bool.true  = Bool.false
Notb Bool.false = Bool.true

// E lógico
Andb (b1: Bool) (b2: Bool) : Bool
Andb Bool.true  b2 = b2
Andb Bool.false b2 = Bool.false

// OU lógico
Orb (b1: Bool) (b2: Bool) : Bool
Orb Bool.true  b2 = Bool.true
Orb Bool.false b2 = b2

As últimas duas funções demonstram como é a sintaxe do Kind para funções de múltiplos argumentos, e também mostra que é possível fazer pattern matching apenas em parte das variáveis da função, não necessariamente todas.

Os casos da última função podem ser testados exaustivamente (todas as possibilidades) como mostrado a seguir, criando a tabela verdade da operação lógica.

TestOrb1 : Equal Bool (Orb Bool.true Bool.false) Bool.true
TestOrb1 = Equal.refl

TestOrb2 : Equal Bool (Orb Bool.false Bool.false) Bool.false
TestOrb2 = Equal.refl

TestOrb3 : Equal Bool (Orb Bool.false Bool.true) Bool.true
TestOrb3 = Equal.refl

TestOrb4 : Equal Bool (Orb Bool.true Bool.true) Bool.true
TestOrb4 = Equal.refl

Nandb

Substitua o buraco "?", completando a função seguinte; então confira se ela está correta usando as constatações a seguir (Análogo a como foi feito para a função Orb). A função retorna Bool.true se qualquer uma de suas entradas for Bool.false

Nandb (b1: Bool) (b2: Bool) : Bool
Nandb b1 b2 = ?

Test_nandb1 : Equal Bool (Nandb Bool.true Bool.false) Bool.true
Test_nandb1 = ?

Test_nandb2 : Equal Bool (Nandb Bool.false Bool.false) Bool.true
Test_nandb2 = ?

Test_nandb3 : Equal Bool (Nandb Bool.false Bool.true) Bool.true
Test_nandb3 = ?

Test_nandb4 : Equal Bool (Nandb Bool.true Bool.true) Bool.false
Test_nandb4 = ?

And3

Faça o mesmo para a função Andb3 abaixo. Essa função deve retornar Bool.true se todas as entradas forem Bool.true, e Bool.false caso contrário

Andb3 (b1: Bool) (b2: Bool) (b3: Bool) : Bool
Andb3 b1 b2 b3 = ?

Test_andb3_1 Equal Bool (Andb3 Bool.true Bool.true Bool.true) Bool.true
Test_andb3_1 = ?

Test_andb3_2 Equal Bool (Andb3 Bool.false Bool.true Bool.true) Bool.false
Test_andb3_2 = ?

Test_andb3_3 Equal Bool (Andb3 Bool.true Bool.false Bool.true) Bool.false
Test_andb3_3 = ?

Test_andb3_4 Equal Bool (Andb3 Bool.true Bool.true Bool.false) Bool.false
Test_andb3_4 = ?