package alba

You can search for identifiers within the package.

in-package search v0.2.0

Alba compiler

Install

sha256=4817038301d3e45bac9edf7e6f2fc8bf0a6d78e76e02ad7ea33ef69bcc17df3b

md5=25234357587126685d64f16236167937

type t

val make : 
  string ->
  Term.typ ->
  (Term.Pi_info.t * Term.typ) list ->
  Sort.t ->
  t

make name kind indices sort

val name : t -> string

val count_indices : t -> int

val has_index : t -> bool

val kind : params -> t -> Term.typ

kind params header returns the kind of the inductive type described by header with the parameters prefixed.

val default_type : int -> params -> t array -> Term.typ

default_type itype params headers the default type of the itypeth member of the family.

val is_well_constructed : int -> params -> t array -> int -> Term.typ -> bool

is_well_constructed itype params headers nargs typ