Library
On this page:
2.1 Nat
Nat
z
s
+
*
Nat=?
2.2 Bool
Bool
true
false
not
2.3 List
List
nil
:  :
2.4 Vector
Vec
nil
:  :
2.5 Fin
Fin
fzero
fsuc
2.6 Equality
refl
8.2

2 Library

2.1 Nat

 (require k/data/nat) package: k

syntax

Nat

type Nat

syntax

z

constructor z

syntax

(s n)

constructor s, n is a Nat

syntax

(+ n m)

n, m are Nat, returns Nat. Plus n and m.

syntax

(* n m)

n, m are Nat, returns Nat. Mutiply n and m.

syntax

(Nat=? n m)

n, m are Nat, returns Bool. return n and m is same(true) or not(false).

2.2 Bool

 (require k/data/bool) package: k

syntax

Bool

type Bool

syntax

true

constructor true

syntax

false

constructor false

syntax

(not b)

b is Bool, returns Bool. return true for false, return false for true.

2.3 List

 (require k/data/list) package: k

syntax

(List A)

type List, A is a Type.

syntax

nil

constructor nil

syntax

(:: e list)

constructor :: e is a A, list is a (List A)

2.4 Vector

 (require k/data/vec) package: k

syntax

(Vec E Len)

type Vec, E is a Type, Len is a Nat.

syntax

nil

constructor nil, Len is z for nil

syntax

(:: e vec)

constructor ::, e is a E, for vec is a (Vec E n), (:: e vec) is a (Vec E (s n))

2.5 Fin

 (require k/data/fin) package: k

syntax

(Fin n)

type Fin, n is a Nat

syntax

fzero

constructor fzero

syntax

(fsuc f)

constructor fsuc, for f is a (Fin n), (fsuc f) is a (Fin (s n))

2.6 Equality

 (require k/equality) package: k

syntax

( x y)

type Martin-Löf identity, since x, y will going to be unified by refl, it provides definition equality.

syntax

refl

constructor refl