{"size": 722, "ext": "scrbl", "max_stars_repo_path": "scribblings/data-type.scrbl", "max_stars_repo_name": "dannypsnl/data-type", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "scribblings/data-type.scrbl", "max_issues_repo_name": "dannypsnl/data-type", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "scribblings/data-type.scrbl", "max_forks_repo_name": "dannypsnl/data-type", "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.5135135135, "max_line_length": 51, "alphanum_fraction": 0.5041551247}
#lang scribble/manual

@require[@for-label[data-type
                    racket/base]]

@title{data-type}
@author{Lîm Tsú-thuàn}

@defmodule[data-type]

@defform[
      (data type-name
            clause ...)
      #:grammar
      [(clause [name param ...])
       (param type
              [param-name type])]
]{
    usage

    @racketblock[
    (data expr
      [Var (name : Symbol)]
      [abs (name : Symbol) (body : expr)]
      [app (fn : expr) (arg : expr)]
      [pi (name : Symbol) (e : expr) (body : expr)]
      [type (level : Integer)]
      [nat]
      [zero]
      [succ (n : expr)]
      [rec expr expr expr expr]
      [id expr expr expr]
      [refl expr]
      [J expr expr expr expr expr expr])
    ]
}
