TFL/usyntax.sig
changeset 3330 ab7161e593c8
parent 3302 404fe31fd8d2
child 3353 9112a2efb9a3
equal deleted inserted replaced
3329:7b43a1e74930 3330:ab7161e593c8
    59   val mk_conj   :{conj1 : term, conj2 : term} -> term
    59   val mk_conj   :{conj1 : term, conj2 : term} -> term
    60   val mk_disj   :{disj1 : term, disj2 : term} -> term
    60   val mk_disj   :{disj1 : term, disj2 : term} -> term
    61   val mk_pabs   :{varstruct : term, body : term} -> term
    61   val mk_pabs   :{varstruct : term, body : term} -> term
    62 
    62 
    63   (* Destruction routines *)
    63   (* Destruction routines *)
    64   val dest_var  : term -> {Name : string, Ty : typ}
       
    65   val dest_const: term -> {Name : string, Ty : typ}
    64   val dest_const: term -> {Name : string, Ty : typ}
    66   val dest_comb : term -> {Rator : term, Rand : term}
    65   val dest_comb : term -> {Rator : term, Rand : term}
    67   val dest_abs  : term -> {Bvar : term, Body : term}
    66   val dest_abs  : term -> {Bvar : term, Body : term}
    68   val dest_eq     : term -> {lhs : term, rhs : term}
    67   val dest_eq     : term -> {lhs : term, rhs : term}
    69   val dest_imp    : term -> {ant : term, conseq : term}
    68   val dest_imp    : term -> {ant : term, conseq : term}
    83   val bvar  : term -> term
    82   val bvar  : term -> term
    84   val body  : term -> term
    83   val body  : term -> term
    85   
    84   
    86 
    85 
    87   (* Query routines *)
    86   (* Query routines *)
    88   val is_var  : term -> bool
       
    89   val is_const: term -> bool
       
    90   val is_comb : term -> bool
       
    91   val is_abs  : term -> bool
       
    92   val is_eq     : term -> bool
    87   val is_eq     : term -> bool
    93   val is_imp    : term -> bool
    88   val is_imp    : term -> bool
    94   val is_forall : term -> bool 
    89   val is_forall : term -> bool 
    95   val is_exists : term -> bool 
    90   val is_exists : term -> bool 
    96   val is_neg    : term -> bool
    91   val is_neg    : term -> bool
   123   val find_term  : (term -> bool) -> term -> term
   118   val find_term  : (term -> bool) -> term -> term
   124   val find_terms : (term -> bool) -> term -> term list
   119   val find_terms : (term -> bool) -> term -> term list
   125   val dest_relation : term -> term * term * term
   120   val dest_relation : term -> term * term * term
   126   val is_WFR : term -> bool
   121   val is_WFR : term -> bool
   127   val ARB : typ -> term
   122   val ARB : typ -> term
   128 
       
   129   (* Prettyprinting *)
       
   130   val Term_to_string : cterm -> string
       
   131 end;
   123 end;