The Library

Fundamental types

(->) : type -> type -> type

The function arrow.

prop : type

The type of propositions (logical formulas).

Negative logical connectives

top : prop

The constant ⊤ from linear logic. Identity of &.

(&) : prop -> prop -> prop

The & (with) connective from linear logic.

(-o) : prop -> prop -> prop

The −∘ (linear implication) connective from linear logic.

forall : (A -> prop) -> prop

The universal quantifier (∀).

(%) : int -> prop -> prop

Adds weight to a negative formula.

(?) : doc -> prop -> prop

Adds documentation to a negative formula.

Positive logical connectives

one : prop

The constant 1 from linear logic. Identity of ⊗ (,).

(,) : prop -> prop -> prop

The ⊗ connective from linear logic.

(;) : prop -> prop -> prop

The ⊕ connective from linear logic.

exists : (A -> prop) -> prop

The existential quantifier (∃).

(=) : A -> A -> prop

Term equality.

Unit

unit : type

The unit type.

unit : unit

The unit term.

Booleans

bool : type

The type of boolean terms.

true : bool

Boolean truth term.

false : bool

Boolean false term.

Integers

int : type

The type of machine integers.

Characters

char : type

The type of unicode characters.

Strings

string : type

The type of packed unicode (UTF-8) strings.

Tuples

tuple : type -> type -> type

The type of tuples.

tup : A -> B -> tuple A B

Constructs a tuple term.

Lists

list : type -> type

The type of lists.

nil : list A

The empty list.

cons : A -> list A -> list A

List cons.

zip : list A -> list B -> list (tuple A B) -> prop

Zip two lists into a third.

elem : A -> list A -> prop

Check membership of list.

Remote procedure calls

rpc : type -> type

The type of remote procedure calls.

hrpc : request -> rpc response

RPC by HTTP request.

Documentation

doc : type

The type of documentation.

summary : string -> doc

Summary documentation.

Actions

action : type

The type of actions.

get : path -> list (tuple string string) -> action response

The HTTP GET action.

head : path -> list (tuple string string) -> action response

The HTTP HEAD action.

post : path -> list (tuple string string) -> string -> action response

The HTTP POST action.

put : path -> list (tuple string string) -> string -> action response

The HTTP PUT action.

delete : path -> list (tuple string string) -> action response

The HTTP DELETE action.

options : path -> list (tuple string string) -> action response

The HTTP OPTIONS action.

Paths

path : type

The type of URI paths.

HTTP

request : type

The type of HTTP requests.

request : method -> path -> list (tuple string string) -> string -> request

HTTP request.

response : type

The type of HTTP responses.

response : int -> list (tuple string string) -> string -> response

HTTP response.

method : type

The type of HTTP methods.

get_ : method

HTTP GET.

head_ : method

HTTP HEAD.

post_ : method

HTTP POST.

put_ : method

HTTP PUT.

delete_ : method

HTTP DELETE.

options_ : method

HTTP OPTION.

patch_ : method

HTTP PATCH.

request_header : string -> string -> request -> prop

State that a request has given header

response_header : string -> string -> response -> prop

State that a response has given header

method : method -> request -> prop

State that a request has given method

path : path -> request -> prop

State that a request has given path

status : int -> response -> prop

State that a response has given status code

status_in : list int -> response -> prop

State that a response has a status code amongst a given list of status codes

request_body : string -> request -> prop

State that a request has a given body

response_body : string -> response -> prop

State that a response has a given body

JSON

json : type

The type of abstract JSON syntax.

json_field : type

The type of abstract JSON fields.

jnull : json

JSON null.

jbool : bool -> json

JSON bool.

jnumber : int -> int -> int -> json

JSON number.

jstring : string -> json

JSON string.

jarray : list json -> json

JSON array.

jobject : list json_field -> json

JSON object.

jfield : string -> json -> json_field

JSON object field.

parse_json : string -> json -> prop

Parse string to abstract JSON.

print_json : json -> string -> prop

Print abstract JSON to string.