package alba

You can search for identifiers within the package.

in-package search v0.2.0

Module `Inductive.Header`Source

Sourcetype t

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

make name kind indices sort

Sourceval name : t -> string

Sourceval count_indices : t -> int

Sourceval has_index : t -> bool

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

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

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

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

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

is_well_constructed itype params headers nargs typ