/[mojave]/metaprl/theories/mc/mp_mc_connect_exp.ml
ViewVC logotype

Diff of /metaprl/theories/mc/mp_mc_connect_exp.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3561 by emre, Sun Mar 31 02:48:35 2002 UTC revision 3562 by emre, Wed Apr 3 08:37:31 2002 UTC
# Line 1111  Line 1111 
1111     else     else
1112        raise (RefineError ("exp_of_term", StringTermError        raise (RefineError ("exp_of_term", StringTermError
1113              ("not an exp",  t)))              ("not an exp",  t)))
1114    
1115    (*
1116     * Convert to and from fundef.
1117     *)
1118    
1119    let term_of_fundef (line, ty, vars, exp) =
1120       mk_fundef_term    (term_of_debug_line line)
1121                         (term_of_ty ty)
1122                         (term_of_list term_of_var vars)
1123                         (term_of_exp exp)
1124    
1125    let fundef_of_term t =
1126       if is_fundef_term t then
1127          let line, ty, vars, exp = dest_fundef_term t in
1128             (debug_line_of_term line),
1129             (ty_of_term ty),
1130             (list_of_term var_of_term vars),
1131             (exp_of_term exp)
1132    
1133       else
1134          raise (RefineError ("fundef_of_term", StringTermError
1135                ("not a fundef", t)))

Legend:
Removed from v.3561  
changed lines
  Added in v.3562

  ViewVC Help
Powered by ViewVC 1.1.26