package dolmen_loop

  1. Overview
  2. Docs
include Typer_intf.Pipe_types with type state := State.t with type ty := Expr.ty with type ty_var := Expr.ty_var with type ty_cst := Expr.ty_cst with type term := Expr.term with type term_var := Expr.term_var with type term_cst := Expr.term_cst with type formula := Expr.formula
val typecheck : State.t -> bool
val reset : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t
val reset_assertions : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t
val push : State.t -> ?loc:Dolmen.Std.Loc.t -> int -> State.t
val pop : State.t -> ?loc:Dolmen.Std.Loc.t -> int -> State.t
val set_logic : State.t -> ?loc:Dolmen.Std.Loc.t -> string -> State.t
val defs : State.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.defs -> State.t * [ `Type_def of Dolmen.Std.Id.t * Expr.ty_cst * Expr.ty_var list * Expr.ty | `Term_def of Dolmen.Std.Id.t * Expr.term_cst * Expr.ty_var list * Expr.term_var list * Expr.term ] list
val decls : State.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> State.t * [ `Type_decl of Expr.ty_cst | `Term_decl of Expr.term_cst ] list
val terms : State.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> State.t * Expr.term list
val formula : State.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> State.t * Expr.formula
val formulas : State.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> State.t * Expr.formula list