type binder = Loc.position * ident option * ghost * pty optiontype param = Loc.position * ident option * ghost * ptyand term_desc = | Ttrue| Tfalse| Tconst of Number.constant| Tident of qualid| Tidapp of qualid * term list| Tapply of term * term| Tinfix of term * ident * term| Tinnfix of term * ident * term| Tbinop of term * Dterm.dbinop * term| Tbinnop of term * Dterm.dbinop * term| Tnot of term| Tif of term * term * term| Tquant of Dterm.dquant * binder list * term list list * term| Tattr of attr * term| Tlet of ident * term * term| Tcase of term * (pattern * term) list| Tcast of term * pty| Ttuple of term list| Trecord of (qualid * term) list| Tupdate of term * (qualid * term) list| Tscope of qualid * term| Tat of term * identtype invariant = term listtype pre = termtype post = Loc.position * (pattern * term) listtype xpost = Loc.position * (qualid * (pattern * term) option) listand expr_desc = | Etrue| Efalse| Econst of Number.constant| Eident of qualid| Eidapp of qualid * expr list| Eapply of expr * expr| Einfix of expr * ident * expr| Einnfix of expr * ident * expr| Elet of ident * ghost * Expr.rs_kind * expr * expr| Erec of fundef list * expr| Efun of binder list * pty option * Ity.mask * spec * expr| Eany of param list * Expr.rs_kind * pty option * Ity.mask * spec| Etuple of expr list| Erecord of (qualid * expr) list| Eupdate of expr * (qualid * expr) list| Eassign of (expr * qualid * expr) list| Esequence of expr * expr| Eif of expr * expr * expr| Ewhile of expr * invariant * variant * expr| Eand of expr * expr| Eor of expr * expr| Enot of expr| Ematch of expr * reg_branch list * exn_branch list| Eabsurd| Epure of term| Eidpur of qualid| Eraise of qualid * expr option| Eexn of ident * pty * Ity.mask * expr| Eoptexn of ident * Ity.mask * expr| Efor of ident * expr * Expr.for_direction * expr * invariant * expr| Eassert of Expr.assertion_kind * term| Escope of qualid * expr| Elabel of ident * expr| Ecast of expr * pty| Eghost of expr| Eattr of attr * exprtype type_decl = {td_loc : Loc.position;td_ident : ident;td_params : ident list;td_vis : visibility;td_mut : bool;td_inv : invariant;td_wit : (qualid * expr) list;td_def : type_def;}type logic_decl = {ld_loc : Loc.position;ld_ident : ident;ld_params : param list;ld_type : pty option;ld_def : term option;}type ind_decl = {in_loc : Loc.position;in_ident : ident;in_params : param list;in_def : (Loc.position * ident * term) list;}type decl = | Dtype of type_decl list| Dlogic of logic_decl list| Dind of Decl.ind_sign * ind_decl list| Dprop of Decl.prop_kind * ident * term| Dlet of ident * ghost * Expr.rs_kind * expr| Drec of fundef list| Dexn of ident * pty * Ity.mask| Dmeta of ident * metarg list| Dclone of qualid * clone_subst list| Duse of qualid