package alba

You can search for identifiers within the package.

in-package search v0.2.0

Alba compiler

Install

dune-project

Dependency

sha256=062f33c55ef39706c4290dff67d5a00bf009051fd757f9352be527f629ae21fc

md5=eb4edc4d6b7e15b83d6397bd34994153

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