package alba

You can search for identifiers within the package.

in-package search v0.2.0

package alba

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

val bruijn_convert : int -> int -> int

module Lambda_info : sig ... end

module Pi_info : sig ... end

module Application_info : sig ... end

type t =

| Sort of Sort.t
| Value of Value.t
| Variable of int
| Typed of t * typ
| Appl of t * t * Application_info.t
| Lambda of typ * t * Lambda_info.t
| Pi of typ * typ * Pi_info.t
| Where of string * typ * t * t
(*
Where (name, tp, exp, def) is equivalent to the beta redex Appl ( Lambda (tp, exp, "name"), def)
*)

and typ = t

and formal_argument = string * typ

and inductive

type t_n = t * int

type typ_n = typ * int

val proposition : t

val any : t

val any_uni : int -> t

val variable : int -> t

val application : t -> t -> t

val implicit_application : t -> t -> t

val binary : t -> t -> t -> t

val applications : t -> t list -> t

val lambda0 : string -> bool -> typ -> t -> t

val product0 : string -> bool -> typ -> typ -> typ

val make_product : string -> bool -> bool -> typ -> typ -> typ

make_product name typed kind arg_typ res_typ

val lambda : string -> typ -> t -> t

val product : string -> typ -> typ -> t

val arrow : typ -> typ -> typ

val lambda_untyped : string -> typ -> t -> t

val product_untyped : string -> typ -> typ -> t

val lambda_in : formal_argument list -> t -> t

val product_in : formal_argument list -> t -> t

val expand_where : string -> typ -> t -> t -> t

Rewrite a where block as an application with a lambda term.

val char : int -> t

char code character value.

val string : string -> t

string str string value.

val number_values : string -> t list

val type_of_sort : Sort.t -> typ

val is_sort : typ -> bool

val pi_sort : typ -> typ -> typ

val split_application : t -> t * (t * Application_info.t) list

split_application t

val map : (int -> int) -> t -> t

map f t

Map the free variables with f

val up_from : int -> int -> t -> t

up_from start delta t: increases all free variables >= start in t by delta

requires: 0 <= delta

val up : int -> t -> t

up delta t: increases all free variables in t by delta

requires: 0 <= delta

val up1 : t -> t

up1 t: increases all free variable in t by 1

val down_from : int -> int -> t -> t option

down_from start delta t: decreases all free variables >= start in t by delta if possible. Returns None it there is a free variable in t with index i < delta.

requires: 0 <= delta

val down : int -> t -> t option

down delta t: decreases all free variables in t by delta if possible. Returns None if there is a free variable in t with index i < delta.

requires: 0 <= delta

val substitute0 : (int -> t) -> bool -> t -> t

substitute0 f beta_reduce t

val substitute : (int -> t) -> t -> t

substitute f term substitutes each free variable i in term by the term f i.

val substitute_with_beta : (int -> t) -> t -> t

substitute f term substitutes each free variable i in term by the term f i and do beta reduction in case that f i appears in a function position and is a function abstraction.

val apply : t -> t -> t

val apply_nargs : t -> int -> Application_info.t -> t

apply_nargs f n mode returns

f (Var (n-1)) ... (Var 0)

where all applications are done with mode mode.

val fold_free : (int -> 'a -> 'a) -> t -> 'a -> 'a

val to_index : int -> t -> t

val to_level : int -> t -> t

val has : (int -> bool) -> t -> bool

has p term does the term have a free variable satisfying p?

val forall : (int -> bool) -> t -> bool

forall p term do all free variables in term satisfy p?

val has_variable : int -> t -> bool

module Monadic (M : Fmlib.Module_types.MONAD) : sig ... end

Monadic functions

module Inductive : sig ... end

Inductive types