equal
deleted
inserted
replaced
99 "-------- build fun for_bdv --------------------------------------------------"; |
99 "-------- build fun for_bdv --------------------------------------------------"; |
100 "-------- build fun for_bdv --------------------------------------------------"; |
100 "-------- build fun for_bdv --------------------------------------------------"; |
101 Subst.program_to_input: Subst.program -> string list; |
101 Subst.program_to_input: Subst.program -> string list; |
102 |
102 |
103 val {scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]; |
103 val {scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]; |
104 val env = [(TermC.str2term "v_v", TermC.str2term "x")] : Subst.T; |
104 val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")] : Subst.T; |
105 |
105 |
106 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env); |
106 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env); |
107 fun scan (Const _) = NONE |
107 fun scan (Const _) = NONE |
108 | scan (Free _) = NONE |
108 | scan (Free _) = NONE |
109 | scan (Var _) = NONE |
109 | scan (Var _) = NONE |