Lines Matching refs:args
243 val ((f,args),rhs) = dest_hd_eqn qtm
525 fun is_mllambda (mlpair(mlpair(x,mlpair(params,mlpair(bdy,n))),args)) =
528 is_mlsexp_list args andalso
540 fun dest_mllambda (mlpair(mlpair(_,mlpair(params,mlpair(bdy,_))),args)) =
541 (dest_mlsexp_list params, bdy, dest_mlsexp_list args)
767 let val (opr,args) = strip_comb tm
769 if opr = ``int_of_num:num->int`` andalso (tl args = [])
770 then (if is_numeral(hd args)
771 then Arbnum.toString(dest_numeral(hd args))
775 else (if opr = ``int_neg:int->int`` andalso (tl args = [])
776 then ("-" ^ dest_integer(hd args))
820 let val (opr,args) = strip_comb tm
823 andalso (length args = 4)
824 andalso is_int_string(dest_integer(el 1 args))
825 andalso is_num_string(dest_integer(el 2 args))
826 andalso is_int_string(dest_integer(el 3 args))
827 andalso is_num_string(dest_integer(el 4 args))
838 let val (_,args) = strip_comb tm
840 (dest_integer(el 1 args),
841 dest_integer(el 2 args),
842 dest_integer(el 3 args),
843 dest_integer(el 4 args))
1002 val args = (flatten o map strip_pair) arg_tuples
1005 if not(length params = length args)
1014 :: map term_to_mlsexp args)
1018 let val (opr,args) = strip_comb tm
1023 (mlsym(abbrevHOLstring(hd args),
1024 abbrevHOLstring(hd(tl args))))
1025 | "ACL2_STRING" => mlstr(abbrevHOLstring(hd args))
1026 | "ACL2_CHARACTER" => mlchr(fromHOLchar(hd args))
1037 (map term_to_mlsexp (opr::args))
1041 then mk_mlsexp_list (map term_to_mlsexp (opr::args)) else
1046 if not(length params = length args)
1055 :: map term_to_mlsexp args)
1121 val (opr, args) = strip_comb l
1126 mk_mlsexp_list(map term_to_mlsexp args),
1360 then let val (params,bdy,args) = dest_mllambda p
1364 map mlsexp_to_term args)
1367 then let val args = map mlsexp_to_term (dest_mlsexp_list y)
1371 (mk_sexp_fun_ty(length args))
1374 (list_mk_comb(opr,args)
1439 let val (opr, args) = strip_comb tm
1443 (zip params args)
1446 ^(list_mk_pair args)``