package alba

You can search for identifiers within the package.

in-package search v0.2.0

alba.albalib
- Albalib
  - Alba_console
    
    Make
    
    IO
    
    Directory
    
    File
    
    In
    
    Out
    
    Read
    
    W
    
    M
    
    Path
    
    Process
    
    Stderr
    
    Stdout
  - Ast
    
    Expression
    
    Operator_expression
    
    Source_entry
  - Build_context
    
    Application
    
    Lambda
    
    Product
    
    Typed
    
    Where
  - Build_expression
  - Build_inductive
  - Build_problem
    
    Print
    
    P
  - Builder
  - Module
    
    Make
    
    Io
    
    Directory
    
    File
    
    In
    
    Out
    
    Read
    
    W
    
    M
    
    Path
    
    Process
    
    Stderr
    
    Stdout
  - Parser_lang
    
    Command
    
    ERROR
    
    Make
    
    Error
    
    Error_printer
    
    PP
    
    Final
    
    Problem
    
    SIG
    
    Error
    
    Error_printer
    
    PP
    
    Source_file
  - Printer
    
    Make
    
    PP
  - Repl
    
    Make
    
    Io
    
    Directory
    
    File
    
    In
    
    Out
    
    Read
    
    W
    
    M
    
    Path
    
    Process
    
    Stderr
    
    Stdout
  - Standard_context
  - Test_builder
    
    Error_print
    
    Expression_parser
    
    Error
    
    Error_printer
    
    PP
    
    Pretty_printer
    
    Term_print
  - Test_inductive
    
    Expression_parser
    
    Error
    
    Error_printer
    
    PP
    
    Inductive_parser
    
    Error
    
    Error_printer
    
    PP
alba.fmlib_js
- Fmlib_js
  - Browser
    
    Decoder
    
    Result
    
    Encoder
    
    Make
    
    App
    
    Attribute
    
    Command
    
    Dom
    
    Subscription
    
    Tree
    
    Attributes
    
    document
    
    event
    
    eventTarget
    
    history
    
    node
    
    primitive_number
    
    style
    
    window
    
    xmlHttpRequest
alba.fmlib_native
- Fmlib_native
  - Native_io
    
    IO
    
    Directory
    
    File
    
    In
    
    Out
    
    Read
    
    W
    
    M
    
    Path
    
    Process
    
    Stderr
    
    Stdout
alba.fmlib_node
- Fmlib_node
  - File_system
  - Io_buffer
    
    Read
    
    W
    
    Write
    
    R
  - Node_io
    
    IO
    
    Directory
    
    File
    
    In
    
    Out
    
    Read
    
    W
    
    M
    
    Path
    
    Process
    
    Stderr
    
    Stdout
  - Path
  - Process
  - Readline

Legend:
Library
Module
Module type
Parameter
Class
Class type

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