Rsyntax
Each function in the Rsyntax structure has a corresponding function in the Psyntax structure, and vice versa. One can flip-flop between the two structures by opening one and then the other. One can also use long identifiers in order to use both syntaxes at once.
- open Rsyntax; open Rsyntax val INST = fn : term subst -> thm -> thm val INST_TYPE = fn : hol_type subst -> thm -> thm val INST_TY_TERM = fn : term subst * hol_type subst -> thm -> thm val SUBST = fn : {thm:thm, var:term} list -> term -> thm -> thm val SUBST_CONV = fn : {thm:thm, var:term} list -> term -> term -> thm val define_new_type_bijections = fn : {ABS:string, REP:string, name:string, tyax:thm} -> thm val dest_abs = fn : term -> {Body:term, Bvar:term} val dest_comb = fn : term -> {Rand:term, Rator:term} val dest_cond = fn : term -> {cond:term, larm:term, rarm:term} val dest_conj = fn : term -> {conj1:term, conj2:term} val dest_cons = fn : term -> {hd:term, tl:term} val dest_const = fn : term -> {Name:string, Ty:hol_type} val dest_disj = fn : term -> {disj1:term, disj2:term} val dest_eq = fn : term -> {lhs:term, rhs:term} val dest_exists = fn : term -> {Body:term, Bvar:term} val dest_forall = fn : term -> {Body:term, Bvar:term} val dest_imp = fn : term -> {ant:term, conseq:term} val dest_let = fn : term -> {arg:term, func:term} val dest_list = fn : term -> {els:term list, ty:hol_type} val dest_pabs = fn : term -> {body:term, varstruct:term} val dest_pair = fn : term -> {fst:term, snd:term} val dest_select = fn : term -> {Body:term, Bvar:term} val dest_type = fn : hol_type -> {Args:hol_type list, Tyop:string} val dest_var = fn : term -> {Name:string, Ty:hol_type} val inst = fn : hol_type subst -> term -> term val match_term = fn : term -> term -> term subst * hol_type subst val match_type = fn : hol_type -> hol_type -> hol_type subst val mk_abs = fn : {Body:term, Bvar:term} -> term val mk_comb = fn : {Rand:term, Rator:term} -> term val mk_cond = fn : {cond:term, larm:term, rarm:term} -> term val mk_conj = fn : {conj1:term, conj2:term} -> term val mk_cons = fn : {hd:term, tl:term} -> term val mk_const = fn : {Name:string, Ty:hol_type} -> term val mk_disj = fn : {disj1:term, disj2:term} -> term val mk_eq = fn : {lhs:term, rhs:term} -> term val mk_exists = fn : {Body:term, Bvar:term} -> term val mk_forall = fn : {Body:term, Bvar:term} -> term val mk_imp = fn : {ant:term, conseq:term} -> term val mk_let = fn : {arg:term, func:term} -> term val mk_list = fn : {els:term list, ty:hol_type} -> term val mk_pabs = fn : {body:term, varstruct:term} -> term val mk_pair = fn : {fst:term, snd:term} -> term val mk_primed_var = fn : {Name:string, Ty:hol_type} -> term val mk_select = fn : {Body:term, Bvar:term} -> term val mk_type = fn : {Args:hol_type list, Tyop:string} -> hol_type val mk_var = fn : {Name:string, Ty:hol_type} -> term val new_binder = fn : {Name:string, Ty:hol_type} -> unit val new_constant = fn : {Name:string, Ty:hol_type} -> unit val new_infix = fn : {Name:string, Prec:int, Ty:hol_type} -> unit val new_recursive_definition = fn : {def:term, fixity:fixity, name:string, rec_axiom:thm} -> thm val new_specification = fn : {consts:{const_name:string, fixity:fixity} list, name:string, sat_thm:thm} -> thm val new_type = fn : {Arity:int, Name:string} -> unit val new_type_definition = fn : {inhab_thm:thm, name:string, pred:term} -> thm val subst = fn : term subst -> term -> term val subst_occs = fn : int list list -> term subst -> term -> term val type_subst = fn : hol_type subst -> hol_type -> hol_type