| Source File | Identifier index | Theory binding index |
|---|
signature FullUnify =
sig
type tyenv
val empty_tyenv : tyenv
val tyunify : (string -> bool) -> tyenv -> (Type.hol_type * Type.hol_type) ->
tyenv option
end
| Source File | Identifier index | Theory binding index |
|---|