equal
deleted
inserted
replaced
55 infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; |
55 infix 9 ` ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x; |
56 |
56 |
57 (* infers the type of a term *) (* FIXME better avoid this low-level stuff *) |
57 (* infers the type of a term *) (* FIXME better avoid this low-level stuff *) |
58 (* similar to Theory.inferT_axm, but allows any type, not just propT *) |
58 (* similar to Theory.inferT_axm, but allows any type, not just propT *) |
59 fun infer sg t = |
59 fun infer sg t = |
60 fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true |
60 fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) Name.context true |
61 ([t],dummyT)); |
61 ([t],dummyT)); |
62 |
62 |
63 (* builds the expression (LAM v. rhs) *) |
63 (* builds the expression (LAM v. rhs) *) |
64 fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs); |
64 fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs); |
65 |
65 |