equal
deleted
inserted
replaced
34 |
34 |
35 (* extension of substitution to type structures *) |
35 (* extension of substitution to type structures *) |
36 consts |
36 consts |
37 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
37 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
38 |
38 |
39 rules |
39 primrec app_subst typ |
40 app_subst_TVar "$ s (TVar n) = s n" |
40 app_subst_TVar "$ s (TVar n) = s n" |
41 app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" |
41 app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" |
|
42 |
42 defs |
43 defs |
43 app_subst_list "$ s == map ($ s)" |
44 app_subst_list "$ s == map ($ s)" |
44 |
45 |
45 (* free_tv s: the type variables occuring freely in the type structure s *) |
46 (* free_tv s: the type variables occuring freely in the type structure s *) |
46 consts |
47 consts |