145 val eq_tvar: (indexname * sort) * (indexname * sort) -> bool |
145 val eq_tvar: (indexname * sort) * (indexname * sort) -> bool |
146 val eq_var: (indexname * typ) * (indexname * typ) -> bool |
146 val eq_var: (indexname * typ) * (indexname * typ) -> bool |
147 val aconv_untyped: term * term -> bool |
147 val aconv_untyped: term * term -> bool |
148 val could_unify: term * term -> bool |
148 val could_unify: term * term -> bool |
149 val strip_abs_eta: int -> term -> (string * typ) list * term |
149 val strip_abs_eta: int -> term -> (string * typ) list * term |
150 val match_bvars: (term * term) * (string * string) list -> (string * string) list |
150 val match_bvars: (term * term) -> (string * string) list -> (string * string) list |
151 val map_abs_vars: (string -> string) -> term -> term |
151 val map_abs_vars: (string -> string) -> term -> term |
152 val rename_abs: term -> term -> term -> term option |
152 val rename_abs: term -> term -> term -> term option |
153 val is_open: term -> bool |
153 val is_open: term -> bool |
154 val is_dependent: term -> bool |
154 val is_dependent: term -> bool |
155 val lambda_name: string * term -> term -> term |
155 val lambda_name: string * term -> term -> term |
609 else (x,y)::al) |
609 else (x,y)::al) |
610 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) |
610 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) |
611 | match_bvs(_,_,al) = al; |
611 | match_bvs(_,_,al) = al; |
612 |
612 |
613 (* strip abstractions created by parameters *) |
613 (* strip abstractions created by parameters *) |
614 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); |
614 fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al); |
615 |
615 |
616 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u |
616 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u |
617 | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) |
617 | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) |
618 | map_abs_vars f t = t; |
618 | map_abs_vars f t = t; |
619 |
619 |