logtk

Core types and algorithms for logic
IN THIS PACKAGE
Parameter #1 Logtk . UnifFramework . Make . X
exception NotInFragment
exception NotUnifiable
type flag_type
val init_flag : flag_type
val flex_state : Flex_state.t
val identify_scope : T.t Scoped.t -> T.t Scoped.t -> T.t * T.t * Scoped.scope * S.t
val identify_scope_l : T.t list Scoped.t -> T.t list Scoped.t -> T.t list * T.t list * Scoped.scope * S.t
val frag_algs : unit -> ( T.t Scoped.t -> T.t Scoped.t -> S.t -> S.t list ) list
val pb_oracle : T.t Scoped.t -> T.t Scoped.t -> flag_type -> S.t -> Scoped.scope -> (S.t * flag_type) option LL.t