alba

Alba compiler
IN THIS PACKAGE
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