package alba

You can search for identifiers within the package.

in-package search v0.2.0

Module `Inductive.Header`

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