On this page:
Type
data
check
typeof
def
8.2

1 Language

This section introduces forms of the language.

syntax

(Type level)

Type is builtin form to represent a type, for example, Nat has type Type, (List Nat) has type Type, and (Type a) has type (Type (add1 a)).

syntax

(data data-bind : type
      constructor ...)
 
data-bind = name
  | (name bind ...)
     
constructor = [name bind ... : type]
     
bind = [name : type]
     
type = name
  | (name type ...)
Here list some classic definition to show how to use data form, you can get more in library: k/data.

(data Nat : Type
      [z : Nat]
      [s (n : Nat) : Nat])
(data (Pair [L : Type] [R : Type]) : Type
      [cons [l : L] [r : R] : (Pair L R)])

syntax

(check type term)

 
type = term
     
term = name
  | (name term ...)
For example, we can have:

(check Nat
       (s (s z)))
(check Bool
       false)

If we using wrong type:

(check Bool
       z)

The syntax error will raise.

syntax

(typeof term)

 
term = name
  | (name term ...)
For example, we can have

(typeof Nat) ; Type
(typeof true) ; Bool

syntax

(def def-bind : type
     clause ...)
 
def-bind = name
  | (name bind ...)
     
clause = [pat ... => term]
     
pat = name
  | (name pat ...)
     
bind = [name : type]
     
type = term
     
term = name
  | (name term ...)
For example, we can have:

(def a : Nat z)

It can use to construct a proof

(def (0+x [x : Nat]) : ( (+ z x) x)
  [x => refl])