Jslogic.JSLCmdtype t = | Fold of JSAsrt.t * (string * (string * JSExpr.t) list) optionFold
*)| Unfold of JSAsrt.t * (string * string) list optionSingle Unfold
*)| GUnfold of stringGlobal unfold
*)| Flash of JSAsrt.tUnfold/fold
*)| If of JSExpr.t * t list * t listIf-then-else
*)| Branch of JSAsrt.pt| ApplyLemma of string * JSExpr.t listLemma
*)| Macro of string * JSExpr.t listMacro
*)| Assert of JSAsrt.t * string listAssert
*)| Assume of JSAsrt.ptAssume
*)| Invariant of JSAsrt.t * string listInvariant
*)| UseSubst of string * (string * JSExpr.t) listval js2jsil :
JSLogicCommon.cc_tbl_type ->
JSLogicCommon.vis_tbl_type ->
JSLogicCommon.pre_fun_tbl_type ->
string ->
string ->
t ->
Jsil_syntax.LCmd.t list