Lines Matching defs:nam
427 (* "tag_ty nam" |--> ("tag_ty","nam") *)
439 (* "pkg::nam" |--> ("pkg","nam") *)
462 => let val (pkg,nam) = split_acl2_name acl2_name
464 mlsym(if pkg = "" then (!current_package) else pkg, nam)
469 else let val (pkg,nam) = split_acl2_name s
471 mlsym(if pkg = "" then (!current_package) else pkg, nam)
571 (* Test for a defun: (DEFUN nam (x1 ... xn) bdy) *)
582 (* Defun destructor: (DEFUN nam (x1 ... xn) bdy) |-->(nam,[x1,...,xn],bdy) *)
587 of [_,nam,params,bdy]
588 => (nam, dest_mlsexp_list params, bdy)
594 (* Defun Constructor: (nam,[x1,...,xn],bdy) |--> (DEFUN nam (x1 ... xn) bdy) *)
596 fun mk_mldefun (nam, params, bdy) =
597 mk_mlsexp_list [mldefun, nam, mk_mlsexp_list params, bdy];
600 (* Test for a defun_sk: (DEFUN-SK nam (x1 ... xn) (QUANT (v1 ... vm) bdy)) *)
623 (* (DEFUN-SK nam (x1 ... xn) (QUANT (v1 ... vm) bdy)) *)
625 (* (nam, [x1,...,xn], quant, qvars, bdy) *)
630 of [_,nam,params,quant_bdy]
633 => (nam, dest_mlsexp_list params,
643 (* (nam,[x1,...,xn],quant,qvars,bdy) *)
645 (* (DEFUN-SK nam (x1 ... xn) (quant qvars bdy)) *)
647 fun mk_mldefun_sk (nam, params, quant, qvars, bdy) =
649 [mldefun_sk, nam, mk_mlsexp_list params,
653 (* Test for a defaxiom: (DEFAXIOM nam bdy) *)
663 (* Defaxiom destructor: (DEFAXIOM nam bdy) |--> (nam,bdy) *)
666 (mlpair(_,mlpair(nam,mlpair(bdy,_)))) = (nam, bdy)
670 (* Defaxiom constructor: (nam,bdy) |--> (DEFAXIOM nam bdy) *)
672 fun mk_mldefaxiom(nam,bdy) =
673 mk_mlsexp_list [mldefaxiom, nam, bdy];
676 (* Test for a defthm: (DEFTHM nam bdy) *)
686 (* Defthm destructor: (DEFTHM nam bdy) |--> (nam,bdy) *)
689 (mlpair(_,mlpair(nam,mlpair(bdy,_)))) = (nam, bdy)
693 (* Defthm constructor: (nam,bdy) |--> (DEFTHM nam bdy) *)
695 fun mk_mldefthm(nam,bdy) =
696 mk_mlsexp_list [mldefthm, nam, bdy];
850 (* mlsym(pkg,nam) |--> "pkg::nam" *)
852 fun mlsym_to_string (sym as mlsym(pkg,nam)) = (pkg^"::"^nam)
1199 fun mlquote_to_string (mlsym(pkg,nam)) =
1200 ("(sym \"" ^ pkg ^ "\" \"" ^ nam ^"\")")
1218 fun mlquote_to_string (mlsym(pkg,nam)) =
1219 ("(sym \"" ^ pkg ^ "\" \"" ^ nam ^"\")")
1237 fun mlquote_to_term (sym as mlsym(pkg,nam)) =
1240 ``sym ^(abbrevMLstring pkg) ^(abbrevMLstring nam)``
1287 (* mlsym(pkg,nam) |--> mk_var("pkg::nam",``:sexp``) *)
1296 (* mlsym(pkg,nam) ty |--> mk_var("pkg::nam",ty) *)
1804 (* defname(defthm(nam, _)) = nam *)
1805 (* defname(defaxiom(nam, _)) = nam *)
1808 | defname(defthm(nam,_)) = nam
1809 | defname(defaxiom(nam,_)) = nam
1829 (* (defun nam (x1 ... xm) bdy) *)
1831 (* defun("nam", ``!x1 ... xm. nam x1 ..., xm = bdy``) *)
1833 (* (defthm nam bdy) *)
1835 (* defthm("nam", ``|= tm``) *)
1837 (* (defaxiom nam bdy) *)
1839 (* defaxiom("nam", ``|= tm``) *)
1858 let val (nam,params,bdy) = dest_mldefun d
1864 subtract (free_vars bdy_tm) (name_to_var nam ty :: param_vars)
1868 ^ snd(dest_mlsym nam)
1871 val sym_name = mlsym_to_string nam
1879 let val (nam,params,quant,qvars,bdy) = dest_mldefun_sk d
1892 subtract (free_vars quant_tm) (name_to_var nam ty :: param_vars)
1896 ^ snd(dest_mlsym nam)
1898 val sym_name = mlsym_to_string nam
1906 let val (nam,bdy) = dest_mldefthm d
1909 val sym_name = mlsym_to_string nam
1915 let val (nam,bdy) = dest_mldefaxiom d
1918 val sym_name = mlsym_to_string nam
1982 | print_acl2def out (defaxiom(nam,tm)) =
1983 (out "; Defaxiom: "; out nam; out "\n";
1987 string_to_mlsym nam,
1990 | print_acl2def out (defthm(nam,tm)) =
1991 (out "; Defthm: "; out nam; out "\n";
1995 string_to_mlsym nam,
2128 (fn (nam,ty) => fn new_nam => declare_names(nam,new_nam))
2156 (fn (nam,ty) => fn new_nam => declare_names(nam,new_nam))