package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Misc functions

alt-ergo-lib
- AltErgoLib
  - Ac
    
    Make
    
    X
    
    S
  - Adt
    
    ALIEN
    
    Shostak
    
    X
  - Adt_rel
  - Arith
    
    Shostak
    
    P
    
    X
    
    Type
    
    X
  - Arrays
    
    ALIEN
    
    Shostak
    
    X
  - Arrays_rel
  - Bitv
    
    ALIEN
    
    Shostak
    
    X
  - Bitv_rel
  - Ccx
    
    Main
    
    S
  - Cnf
  - Commands
  - Compat
    
    Seq
    
    String
  - D_cnf
  - D_loop
    
    Header
    
    Parser
    
    Pipeline
    
    Typer
    
    Typer_Pipe
  - Emap
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Enum
    
    ALIEN
    
    Shostak
    
    X
  - Enum_rel
  - Errors
  - Explanation
  - Expr
    
    BV
    
    Core
    
    Ints
  - Fpa_rounding
  - Frontend
    
    Make
    
    SAT
    
    S
  - Fun_sat
    
    Make
    
    Th
  - Gc_debug
  - Hconsing
    
    HASHED
    
    Make
    
    H
    
    S
  - Hstring
  - Iheap
  - Inequalities
    
    Container_SIG
    
    Make
    
    MINEQS
    
    P
    
    FM
    
    MINEQS
    
    P
    
    S
    
    MINEQS
    
    P
  - Input
    
    S
  - Instances
    
    Make
    
    X
    
    S
  - IntervalCalculus
  - Intervals
  - Ite
    
    ALIEN
    
    Shostak
    
    X
  - Ite_rel
  - Lists
  - Loc
  - Matching
    
    Arg
    
    Make
    
    X
    
    S
  - Matching_types
  - ModelMap
  - Models
  - MyUnix
  - My_zip
  - Numbers
    
    Q
    
    Z
  - Options
    
    Output
    
    Time
  - Parsed
  - Parsed_interface
  - Polynome
    
    EXTENDED_Polynome
    
    Make
    
    X
    
    S
    
    T
  - Printer
  - Profiling
  - Records
    
    ALIEN
    
    Shostak
    
    X
  - Records_rel
  - Relation
  - Sat_solver
  - Sat_solver_sig
    
    S
    
    SatContainer
    
    Make
    
    Th
  - Satml
    
    Make
    
    Th
    
    SAT_ML
  - Satml_frontend
    
    Make
    
    Th
  - Satml_frontend_hybrid
    
    Make
    
    Th
  - Satml_types
    
    ATOM
    
    Atom
    
    FLAT_FORMULA
    
    Flat_Formula
    
    Proxy_formula
  - Shostak
    
    Ac
    
    Adt
    
    Arith
    
    Arrays
    
    Bitv
    
    Combine
    
    Enum
    
    Ite
    
    Polynome
    
    Records
  - Sig
    
    SHOSTAK
    
    X
  - Sig_rel
    
    RELATION
  - Steps
  - Symbols
    
    Map
  - Th_util
  - Theories
  - Theory
    
    Main_Default
    
    Main_Empty
    
    S
  - Timers
  - Ty
  - Typechecker
  - Typed
  - Uf
    
    LX
  - Use
  - Util
  - Var
  - Vec
  - Version
  - Xliteral
    
    Make
    
    X
    
    OrderedType
    
    S

Legend:
Library
Module
Module type
Parameter
Class
Class type

Lists utilies

This modules defines some helper functions on lists

Misc functions

val is_empty : 'a list -> bool

Is the list empty?

val to_seq : 'a list -> 'a Stdlib.Seq.t

Iterate on the list

val apply : ('a -> 'a) -> 'a list -> 'a list * bool

apply f [a_1; ...; a_n] returns a couple [f a_1; ...; f a_n], same same such that: (1) "same" is true if and only if a_i == a_i for each i; and (2) if same is true, then the resulting list is physically equal to the argument *

val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool

similar to function apply, but the elements of the list are couples *

val find_opt : ('a -> bool) -> 'a list -> 'a option

Tries and find the first element of the list satisfying the predicate.

val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int

compare cmp l1 l2 compares the lists l1 and l2 using the comparison function cmp on elements.

val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool

equal eq l1 l2 holds when the two input lists have the same length and for each pair of elements ai, bi at the same position in l1 and l2 respectively, we have eq ai bi.

This is a backport of List.equal from OCaml 4.12.0