{"size": 1104, "ext": "scrbl", "max_stars_repo_path": "scribblings/library.scrbl", "max_stars_repo_name": "CYBAI/k", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "scribblings/library.scrbl", "max_issues_repo_name": "CYBAI/k", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "scribblings/library.scrbl", "max_forks_repo_name": "CYBAI/k", "max_forks_repo_forks_event_min_datetime": null, "max_forks_repo_forks_event_max_datetime": null}
{"max_stars_count": null, "max_issues_count": null, "max_forks_count": null, "avg_line_length": 19.3684210526, "max_line_length": 75, "alphanum_fraction": 0.6222826087}
#lang scribble/manual
@require[@for-label[k]
         "helper.rkt"]

@title[#:tag "library"]{Library}

@defmodule[k/data/nat]

@defidform[Nat]{
    type @code{Nat}
    @defsubidform[z]{constructor @code{z}}
    @defsubform[(s n)]{constructor @code{s}}
}

@defform[(+ n m)]{
    Plus @code{n} and @code{m}.
}

@defform[(* n m)]{
    Mutiply @code{n} and @code{m}.
}

@defform[(Nat=? n m)]{
    return @code{n} and @code{m} is same(@code{true}) or not(@code{false}).
}

@defmodule[k/data/bool]

@defidform[Bool]{
    type @code{Bool}
    @defsubidform[true]{constructor @code{true}}
    @defsubidform[false]{constructor @code{false}}
}

@defmodule[k/data/list]

@defform[(List A)]{
    type @code{List}
    @defsubidform[nil]{constructor @code{nil}}
    @defsubform[(:: e list)]{constructor @code{::}}
}

@defmodule[k/data/vec]

@defform[(Vec E Len)]{
    type @code{Vec}
    @defsubidform[nil]{constructor @code{nil}}
    @defsubform[(:: e vec)]{constructor @code{::}}
}

@defmodule[k/equality]

@defform[(≡ x y)]{
    type @code{≡}: Martin-Löf identity
    @defsubidform[refl]{constructor @code{refl}}
}
