/[mojave]/metaprl/library/basic.ml
ViewVC logotype

Diff of /metaprl/library/basic.ml

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

revision 2921 by nogin, Fri Oct 22 01:07:59 1999 UTC revision 2922 by lolorigo, Thu Mar 16 19:52:02 2000 UTC
# Line 73  Line 73 
73            op_params = bparms }            op_params = bparms }
74          -> (aopname = bopname & listeq parmeq aparms bparms))          -> (aopname = bopname & listeq parmeq aparms bparms))
75    
   
 let nuprl5_opname_p opn = stringeq opn nuprl5_opname  
   
   
76  open Hashtbl  open Hashtbl
77    
78  (*      TODO PERF  (*      TODO PERF
# Line 96  Line 92 
92   * common terms   * common terms
93   *)   *)
94    
 let mk_nuprl5_op pl = mk_op nuprl5_opname pl  
   
95  let imessage_parameter = make_param (Token "!message")  let imessage_parameter = make_param (Token "!message")
96  let imessage_op parms = mk_nuprl5_op (imessage_parameter :: parms)  let imessage_op parms = mk_nuprl5_op (imessage_parameter :: parms)
97    
# Line 241  Line 235 
235      Token s -> s      Token s -> s
236    |_ -> error ["parameter"; "token"; "not"] [] []    |_ -> error ["parameter"; "token"; "not"] [] []
237    
238    let ipui_addr_parameter = make_param (Token "!pui_addr")
239    let number_of_ipui_addr_term t =
240      match dest_param (parameter_of_carrier ipui_addr_parameter t) with
241        Number (Mp_num.Int n) -> n
242      |_ -> error ["term"; "!pui_addr"; "parameter type"] [] [t]
243    
244  let number_of_inatural_term t =  let number_of_inatural_term t =
245    match dest_param (parameter_of_carrier inatural_parameter t) with    match dest_param (parameter_of_carrier inatural_parameter t) with

Legend:
Removed from v.2921  
changed lines
  Added in v.2922

  ViewVC Help
Powered by ViewVC 1.1.26