Structure FullUnify


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

HOL 4, Kananaskis-13